Theorem reximdai 3238

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3052  df-rex 3061

This theorem is referenced by:  2reurex  3718  fompt  7063  tz7.49  8376  hsmexlem2  10337  acunirnmpt2  32738  acunirnmpt2f  32739  locfinreflem  33997  cmpcref  34007  fvineqsneq  37617  indexdom  37935  filbcmb  37941  cdlemefr29exN  40662  rexanuz3  45340  reximdd  45392  disjrnmpt2  45432  disjinfi  45436  iunmapsn  45461  infnsuprnmpt  45494  rnmptbdlem  45499  supxrge  45583  suplesup  45584  infxr  45611  allbutfi  45637  supxrunb3  45643  infxrunb3rnmpt  45672  infrpgernmpt  45709  limsupre  45885  limsupub  45948  limsupre3lem  45976  limsupgtlem  46021  xlimmnfvlem1  46076  xlimpnfvlem1  46080  stoweidlem31  46275  stoweidlem34  46278  fourierdlem73  46423  sge0pnffigt  46640  sge0ltfirp  46644  sge0reuzb  46692  iundjiun  46704  ovnlerp  46806  smflimlem4  47018  smflimsuplem7  47070