Theorem reximdai 3267

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

Syntax hints:   → wi 4  Ⅎwnf 1806   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-ral 3080  df-rex 3090

This theorem is referenced by:  2reurex  3726  fompt  7103  tz7.49  8420  hsmexlem2  10399  acunirnmpt2  32913  acunirnmpt2f  32914  locfinreflem  34142  cmpcref  34152  fvineqsneq  37913  indexdom  38240  filbcmb  38246  cdlemefr29exN  41033  rexanuz3  45673  reximdd  45725  disjrnmpt2  45765  disjinfi  45769  iunmapsn  45792  infnsuprnmpt  45824  rnmptbdlem  45829  supxrge  45913  suplesup  45914  infxr  45941  allbutfi  45967  supxrunb3  45973  infxrunb3rnmpt  46001  infrpgernmpt  46038  limsupre  46214  limsupub  46277  limsupre3lem  46305  limsupgtlem  46350  xlimmnfvlem1  46405  xlimpnfvlem1  46409  stoweidlem31  46604  stoweidlem34  46607  fourierdlem73  46752  sge0pnffigt  46969  sge0ltfirp  46973  sge0reuzb  47021  iundjiun  47033  ovnlerp  47135  smflimlem4  47347  smflimsuplem7  47399