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