Theorem reximdai 3265

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3078  df-rex 3088

This theorem is used by:  2reurex  3718  fompt  7110  tz7.49  8439  hsmexlem2  10486  acunirnmpt2  33236  acunirnmpt2f  33237  locfinreflem  34454  cmpcref  34464  fvineqsneq  38303  indexdom  38636  filbcmb  38642  cdlemefr29exN  41427  rexanuz3  46054  reximdd  46106  disjrnmpt2  46146  disjinfi  46150  iunmapsn  46173  infnsuprnmpt  46205  rnmptbdlem  46210  supxrge  46294  suplesup  46295  infxr  46322  allbutfi  46348  supxrunb3  46354  infxrunb3rnmpt  46382  infrpgernmpt  46419  limsupre  46595  limsupub  46658  limsupre3lem  46686  limsupgtlem  46731  xlimmnfvlem1  46786  xlimpnfvlem1  46790  stoweidlem31  46985  stoweidlem34  46988  fourierdlem73  47133  sge0pnffigt  47350  sge0ltfirp  47354  sge0reuzb  47402  iundjiun  47414  ovnlerp  47516  smflimlem4  47728  smflimsuplem7  47780