Theorem reximdai 3311

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)

Hypotheses

Ref	Expression
reximdai.1	⊢ Ⅎ𝑥𝜑
reximdai.2	⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
reximdai	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Proof of Theorem reximdai

Step	Hyp	Ref	Expression
1		reximdai.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		reximdai.2	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	1, 2	ralrimi 3216	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
4		rexim 3241	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
5	3, 4	syl 17	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1780   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  2reurex  3749  tz7.49  8080  hsmexlem2  9848  acunirnmpt2  30404  acunirnmpt2f  30405  locfinreflem  31104  cmpcref  31114  fvineqsneq  34692  indexdom  35008  filbcmb  35014  cdlemefr29exN  37537  rexanuz3  41360  reximdd  41419  disjrnmpt2  41447  fompt  41451  disjinfi  41452  iunmapsn  41478  infnsuprnmpt  41520  rnmptbdlem  41525  supxrge  41604  suplesup  41605  infxr  41633  allbutfi  41663  supxrunb3  41670  infxrunb3rnmpt  41700  infrpgernmpt  41739  limsupre  41920  limsupub  41983  limsupre3lem  42011  limsupgtlem  42056  xlimmnfvlem1  42111  xlimpnfvlem1  42115  stoweidlem31  42315  stoweidlem34  42318  fourierdlem73  42463  sge0pnffigt  42677  sge0ltfirp  42681  sge0reuzb  42729  iundjiun  42741  ovnlerp  42843  smflimlem4  43049  smflimsuplem7  43099