Rule. disj_elim
(H1 ⊢ A ∨ B) → (H2 ∧ A ⊢ C) → (H3 ∧ B ⊢ C) → (H1 ∧ H2 ∧ H3 ⊢ C)