case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp only [Formula.primeSet] at h1
  simp at h1
  tauto
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
no goals