Theorem reximdai 3241

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

Syntax hints:   → wi 4  Ⅎwnf 1790   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-ral 3054  df-rex 3064

This theorem is referenced by:  2reurex  3701  fompt  7059  tz7.49  8374  hsmexlem2  10340  acunirnmpt2  32752  acunirnmpt2f  32753  locfinreflem  34024  cmpcref  34034  fvineqsneq  37774  indexdom  38101  filbcmb  38107  cdlemefr29exN  40894  rexanuz3  45543  reximdd  45595  disjrnmpt2  45635  disjinfi  45639  iunmapsn  45662  infnsuprnmpt  45694  rnmptbdlem  45699  supxrge  45783  suplesup  45784  infxr  45811  allbutfi  45837  supxrunb3  45843  infxrunb3rnmpt  45871  infrpgernmpt  45908  limsupre  46084  limsupub  46147  limsupre3lem  46175  limsupgtlem  46220  xlimmnfvlem1  46275  xlimpnfvlem1  46279  stoweidlem31  46474  stoweidlem34  46477  fourierdlem73  46622  sge0pnffigt  46839  sge0ltfirp  46843  sge0reuzb  46891  iundjiun  46903  ovnlerp  47005  smflimlem4  47217  smflimsuplem7  47269