apply IsDeduct.axiom_
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))