Rule. ex_elim
(nf u (H1 ∧ H2 ∧ B ∧ ∃x. P x)) → (H1 ⊢ ∃x. P x) → (H2 ∧ P u ⊢ B) → (H1 ∧ H2 ⊢ B)