Theorem reximdai 3258

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

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

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-ral 3062  df-rex 3071

This theorem is referenced by:  2reurex  3756  fompt  7119  tz7.49  8447  hsmexlem2  10424  acunirnmpt2  31923  acunirnmpt2f  31924  locfinreflem  32889  cmpcref  32899  fvineqsneq  36379  indexdom  36688  filbcmb  36694  cdlemefr29exN  39359  rexanuz3  43867  reximdd  43923  disjrnmpt2  43966  disjinfi  43970  iunmapsn  43995  infnsuprnmpt  44033  rnmptbdlem  44038  supxrge  44127  suplesup  44128  infxr  44156  allbutfi  44182  supxrunb3  44188  infxrunb3rnmpt  44217  infrpgernmpt  44254  limsupre  44436  limsupub  44499  limsupre3lem  44527  limsupgtlem  44572  xlimmnfvlem1  44627  xlimpnfvlem1  44631  stoweidlem31  44826  stoweidlem34  44829  fourierdlem73  44974  sge0pnffigt  45191  sge0ltfirp  45195  sge0reuzb  45243  iundjiun  45255  ovnlerp  45357  smflimlem4  45569  smflimsuplem7  45621