Theorem reximdai 3239

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

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

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 3052  df-rex 3062

This theorem is referenced by:  2reurex  3706  fompt  7070  tz7.49  8384  hsmexlem2  10349  acunirnmpt2  32733  acunirnmpt2f  32734  locfinreflem  33984  cmpcref  33994  fvineqsneq  37728  indexdom  38055  filbcmb  38061  cdlemefr29exN  40848  rexanuz3  45526  reximdd  45578  disjrnmpt2  45618  disjinfi  45622  iunmapsn  45646  infnsuprnmpt  45679  rnmptbdlem  45684  supxrge  45768  suplesup  45769  infxr  45796  allbutfi  45822  supxrunb3  45828  infxrunb3rnmpt  45856  infrpgernmpt  45893  limsupre  46069  limsupub  46132  limsupre3lem  46160  limsupgtlem  46205  xlimmnfvlem1  46260  xlimpnfvlem1  46264  stoweidlem31  46459  stoweidlem34  46462  fourierdlem73  46607  sge0pnffigt  46824  sge0ltfirp  46828  sge0reuzb  46876  iundjiun  46888  ovnlerp  46990  smflimlem4  47202  smflimsuplem7  47254