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

Syntax hints:   → wi 4  Ⅎwnf 1790   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-ral 3055  df-rex 3065

This theorem is referenced by:  2reurex  3708  fompt  7066  tz7.49  8381  hsmexlem2  10347  acunirnmpt2  32759  acunirnmpt2f  32760  locfinreflem  34031  cmpcref  34041  fvineqsneq  37781  indexdom  38108  filbcmb  38114  cdlemefr29exN  40901  rexanuz3  45550  reximdd  45602  disjrnmpt2  45642  disjinfi  45646  iunmapsn  45669  infnsuprnmpt  45701  rnmptbdlem  45706  supxrge  45790  suplesup  45791  infxr  45818  allbutfi  45844  supxrunb3  45850  infxrunb3rnmpt  45878  infrpgernmpt  45915  limsupre  46091  limsupub  46154  limsupre3lem  46182  limsupgtlem  46227  xlimmnfvlem1  46282  xlimpnfvlem1  46286  stoweidlem31  46481  stoweidlem34  46484  fourierdlem73  46629  sge0pnffigt  46846  sge0ltfirp  46850  sge0reuzb  46898  iundjiun  46910  ovnlerp  47012  smflimlem4  47224  smflimsuplem7  47276