first
| apply ValidOnFrame.verum
| apply ValidOnFrame.imply₁
| apply ValidOnFrame.imply₂
| apply ValidOnFrame.disj₁
| apply ValidOnFrame.disj₂
| apply ValidOnFrame.disj₃
| apply ValidOnFrame.conj₁
| apply ValidOnFrame.conj₂
| apply ValidOnFrame.conj₃
case disj₃
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
p : Formula α
F : Frame' α
hF : F ∈ 𝔽(Ax(𝓓))
p✝ q✝ r✝ : Formula α
⊢ F ⊧ (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
no goals