Theorem reximdai 3240

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3053  df-rex 3063

This theorem is referenced by:  2reurex  3707  fompt  7064  tz7.49  8377  hsmexlem2  10340  acunirnmpt2  32748  acunirnmpt2f  32749  locfinreflem  34000  cmpcref  34010  fvineqsneq  37742  indexdom  38069  filbcmb  38075  cdlemefr29exN  40862  rexanuz3  45544  reximdd  45596  disjrnmpt2  45636  disjinfi  45640  iunmapsn  45664  infnsuprnmpt  45697  rnmptbdlem  45702  supxrge  45786  suplesup  45787  infxr  45814  allbutfi  45840  supxrunb3  45846  infxrunb3rnmpt  45874  infrpgernmpt  45911  limsupre  46087  limsupub  46150  limsupre3lem  46178  limsupgtlem  46223  xlimmnfvlem1  46278  xlimpnfvlem1  46282  stoweidlem31  46477  stoweidlem34  46480  fourierdlem73  46625  sge0pnffigt  46842  sge0ltfirp  46846  sge0reuzb  46894  iundjiun  46906  ovnlerp  47008  smflimlem4  47220  smflimsuplem7  47272