have l₂ : t ⊨ g := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₂⟩
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
⊢ t⊨f&g
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
l₂ : t⊨g
⊢ t⊨f&g