case prop_2_ h1_phi h1_psi h1_chi =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_2_
F h1_phi h1_psi h1_chi : Formula
⊢ IsDeduct ∅ ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
no goals