apply IsDeduct.axiom_
case a.a.a
P Q : Formula
⊢ IsDeduct ∅ (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))
case a.a.a.a
P Q : Formula
⊢ IsAxiom (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))