Theorem reximdai 3234

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3048  df-rex 3057

This theorem is referenced by:  2reurex  3719  fompt  7051  tz7.49  8364  hsmexlem2  10318  acunirnmpt2  32640  acunirnmpt2f  32641  locfinreflem  33851  cmpcref  33861  fvineqsneq  37452  indexdom  37780  filbcmb  37786  cdlemefr29exN  40447  rexanuz3  45139  reximdd  45191  disjrnmpt2  45231  disjinfi  45235  iunmapsn  45260  infnsuprnmpt  45293  rnmptbdlem  45298  supxrge  45383  suplesup  45384  infxr  45411  allbutfi  45437  supxrunb3  45443  infxrunb3rnmpt  45472  infrpgernmpt  45509  limsupre  45685  limsupub  45748  limsupre3lem  45776  limsupgtlem  45821  xlimmnfvlem1  45876  xlimpnfvlem1  45880  stoweidlem31  46075  stoweidlem34  46078  fourierdlem73  46223  sge0pnffigt  46440  sge0ltfirp  46444  sge0reuzb  46492  iundjiun  46504  ovnlerp  46606  smflimlem4  46818  smflimsuplem7  46870