Theorem ex_weaken_conj

Proof
01. 1 ⊢ ∀x. P x → Q x, hypo.
02. 2 ⊢ ∃x. P x ∧ R x, hypo.
03. 3 ⊢ P u ∧ R u, hypo.
04. 1 ⊢ P u → Q u, uq_elim 1.
05. 3 ⊢ P u, conj_eliml 3.
06. 1, 3 ⊢ Q u, subj_elim 4 5.
07. 3 ⊢ R u, conj_elimr 3.
08. 1, 3 ⊢ Q u ∧ R u, conj_intro 6 7.
09. 1, 3 ⊢ ∃x. Q x ∧ R x, ex_intro 8.
10. 1, 2 ⊢ ∃x. Q x ∧ R x, ex_elim 2 9.
ex_weaken_conj. ⊢ (∀x. P x → Q x) → (∃x. P x ∧ R x) →
  (∃x. Q x ∧ R x), subj_intro_ii 10.