apply deducible_of_validOnCanonicelModel.mp
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ 𝓓 ⊢! p
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ CanonicalModel 𝓓 ⊧ p