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