Theorem reximdai 3267

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

Syntax hints:   → wi 4  Ⅎwnf 1781   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-ral 3068  df-rex 3077

This theorem is referenced by:  2reurex  3782  fompt  7152  tz7.49  8501  hsmexlem2  10496  acunirnmpt2  32678  acunirnmpt2f  32679  locfinreflem  33786  cmpcref  33796  fvineqsneq  37378  indexdom  37694  filbcmb  37700  cdlemefr29exN  40359  rexanuz3  44998  reximdd  45053  disjrnmpt2  45095  disjinfi  45099  iunmapsn  45124  infnsuprnmpt  45159  rnmptbdlem  45164  supxrge  45253  suplesup  45254  infxr  45282  allbutfi  45308  supxrunb3  45314  infxrunb3rnmpt  45343  infrpgernmpt  45380  limsupre  45562  limsupub  45625  limsupre3lem  45653  limsupgtlem  45698  xlimmnfvlem1  45753  xlimpnfvlem1  45757  stoweidlem31  45952  stoweidlem34  45955  fourierdlem73  46100  sge0pnffigt  46317  sge0ltfirp  46321  sge0reuzb  46369  iundjiun  46381  ovnlerp  46483  smflimlem4  46695  smflimsuplem7  46747