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  3755  tz7.49  8441  hsmexlem2  10418  acunirnmpt2  31872  acunirnmpt2f  31873  locfinreflem  32808  cmpcref  32818  fvineqsneq  36281  indexdom  36590  filbcmb  36596  cdlemefr29exN  39261  rexanuz3  43770  reximdd  43826  disjrnmpt2  43871  fompt  43875  disjinfi  43876  iunmapsn  43901  infnsuprnmpt  43940  rnmptbdlem  43945  supxrge  44034  suplesup  44035  infxr  44063  allbutfi  44089  supxrunb3  44095  infxrunb3rnmpt  44124  infrpgernmpt  44161  limsupre  44343  limsupub  44406  limsupre3lem  44434  limsupgtlem  44479  xlimmnfvlem1  44534  xlimpnfvlem1  44538  stoweidlem31  44733  stoweidlem34  44736  fourierdlem73  44881  sge0pnffigt  45098  sge0ltfirp  45102  sge0reuzb  45150  iundjiun  45162  ovnlerp  45264  smflimlem4  45476  smflimsuplem7  45528