Theorem reximdai 3248

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 3244	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
4		rexim 3078	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
5	3, 4	syl 17	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3053  df-rex 3062

This theorem is referenced by:  2reurex  3748  fompt  7113  tz7.49  8464  hsmexlem2  10446  acunirnmpt2  32643  acunirnmpt2f  32644  locfinreflem  33876  cmpcref  33886  fvineqsneq  37435  indexdom  37763  filbcmb  37769  cdlemefr29exN  40426  rexanuz3  45100  reximdd  45152  disjrnmpt2  45192  disjinfi  45196  iunmapsn  45221  infnsuprnmpt  45254  rnmptbdlem  45259  supxrge  45345  suplesup  45346  infxr  45374  allbutfi  45400  supxrunb3  45406  infxrunb3rnmpt  45435  infrpgernmpt  45472  limsupre  45650  limsupub  45713  limsupre3lem  45741  limsupgtlem  45786  xlimmnfvlem1  45841  xlimpnfvlem1  45845  stoweidlem31  46040  stoweidlem34  46043  fourierdlem73  46188  sge0pnffigt  46405  sge0ltfirp  46409  sge0reuzb  46457  iundjiun  46469  ovnlerp  46571  smflimlem4  46783  smflimsuplem7  46835