simp only [Formula.primeSet] at h1
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ (phi.iff_ psi).primeSet
⊢ F'.IsPrime
F' phi psi : Formula
phi_ih : F' ∈ phi.primeSet → F'.IsPrime
psi_ih : F' ∈ psi.primeSet → F'.IsPrime
h1 : F' ∈ phi.primeSet ∪ psi.primeSet
⊢ F'.IsPrime