Theorem reximdai 3259

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

Syntax hints:   → wi 4  Ⅎwnf 1780   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-ral 3060  df-rex 3069

This theorem is referenced by:  2reurex  3769  fompt  7138  tz7.49  8484  hsmexlem2  10465  acunirnmpt2  32677  acunirnmpt2f  32678  locfinreflem  33801  cmpcref  33811  fvineqsneq  37395  indexdom  37721  filbcmb  37727  cdlemefr29exN  40385  rexanuz3  45036  reximdd  45091  disjrnmpt2  45131  disjinfi  45135  iunmapsn  45160  infnsuprnmpt  45195  rnmptbdlem  45200  supxrge  45288  suplesup  45289  infxr  45317  allbutfi  45343  supxrunb3  45349  infxrunb3rnmpt  45378  infrpgernmpt  45415  limsupre  45597  limsupub  45660  limsupre3lem  45688  limsupgtlem  45733  xlimmnfvlem1  45788  xlimpnfvlem1  45792  stoweidlem31  45987  stoweidlem34  45990  fourierdlem73  46135  sge0pnffigt  46352  sge0ltfirp  46356  sge0reuzb  46404  iundjiun  46416  ovnlerp  46518  smflimlem4  46730  smflimsuplem7  46782