apply IsAxiom.prop_2_
case a.a.a
P Q : Formula
⊢ IsAxiom
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))
no goals