Theorem reximdai 3260

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

Syntax hints:   → wi 4  Ⅎwnf 1782   ∈ wcel 2107  ∀wral 3060  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-ral 3061  df-rex 3070

This theorem is referenced by:  2reurex  3765  fompt  7137  tz7.49  8486  hsmexlem2  10468  acunirnmpt2  32671  acunirnmpt2f  32672  locfinreflem  33840  cmpcref  33850  fvineqsneq  37414  indexdom  37742  filbcmb  37748  cdlemefr29exN  40405  rexanuz3  45106  reximdd  45158  disjrnmpt2  45198  disjinfi  45202  iunmapsn  45227  infnsuprnmpt  45262  rnmptbdlem  45267  supxrge  45354  suplesup  45355  infxr  45383  allbutfi  45409  supxrunb3  45415  infxrunb3rnmpt  45444  infrpgernmpt  45481  limsupre  45661  limsupub  45724  limsupre3lem  45752  limsupgtlem  45797  xlimmnfvlem1  45852  xlimpnfvlem1  45856  stoweidlem31  46051  stoweidlem34  46054  fourierdlem73  46199  sge0pnffigt  46416  sge0ltfirp  46420  sge0reuzb  46468  iundjiun  46480  ovnlerp  46582  smflimlem4  46794  smflimsuplem7  46846