Theorem reximdai 3242

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

Syntax hints:   → wi 4  Ⅎwnf 1786   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-ral 3069  df-rex 3070

This theorem is referenced by:  2reurex  3695  tz7.49  8264  hsmexlem2  10171  acunirnmpt2  30983  acunirnmpt2f  30984  locfinreflem  31776  cmpcref  31786  fvineqsneq  35569  indexdom  35878  filbcmb  35884  cdlemefr29exN  38402  rexanuz3  42605  reximdd  42660  disjrnmpt2  42685  fompt  42689  disjinfi  42690  iunmapsn  42716  infnsuprnmpt  42755  rnmptbdlem  42760  supxrge  42836  suplesup  42837  infxr  42865  allbutfi  42892  supxrunb3  42898  infxrunb3rnmpt  42927  infrpgernmpt  42964  limsupre  43141  limsupub  43204  limsupre3lem  43232  limsupgtlem  43277  xlimmnfvlem1  43332  xlimpnfvlem1  43336  stoweidlem31  43531  stoweidlem34  43534  fourierdlem73  43679  sge0pnffigt  43893  sge0ltfirp  43897  sge0reuzb  43945  iundjiun  43957  ovnlerp  44059  smflimlem4  44265  smflimsuplem7  44315