apply IsDeduct.axiom_
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi