apply iff_valid_on_canonicalModel_deducible.mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ CanonicalModel L ⊧ p
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p