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  3720  fompt  7072  tz7.49  8386  hsmexlem2  10349  acunirnmpt2  32749  acunirnmpt2f  32750  locfinreflem  34017  cmpcref  34027  fvineqsneq  37664  indexdom  37982  filbcmb  37988  cdlemefr29exN  40775  rexanuz3  45452  reximdd  45504  disjrnmpt2  45544  disjinfi  45548  iunmapsn  45572  infnsuprnmpt  45605  rnmptbdlem  45610  supxrge  45694  suplesup  45695  infxr  45722  allbutfi  45748  supxrunb3  45754  infxrunb3rnmpt  45783  infrpgernmpt  45820  limsupre  45996  limsupub  46059  limsupre3lem  46087  limsupgtlem  46132  xlimmnfvlem1  46187  xlimpnfvlem1  46191  stoweidlem31  46386  stoweidlem34  46389  fourierdlem73  46534  sge0pnffigt  46751  sge0ltfirp  46755  sge0reuzb  46803  iundjiun  46815  ovnlerp  46917  smflimlem4  47129  smflimsuplem7  47181