have l₃ := (BTheorem.mp (BTheorem.adj l₁ l₂) BTheorem.orE)
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
⊢ f ∈ ▲{g¦h}
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
l₃ : BTheorem (g¦h⊃f)
⊢ f ∈ ▲{g¦h}