Theorem reximdai 3264

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-ral 3077  df-rex 3087

This theorem is used by:  2reurex  3717  fompt  7119  tz7.49  8459  hsmexlem2  10509  acunirnmpt2  33302  acunirnmpt2f  33303  locfinreflem  34519  cmpcref  34529  srepdflem2  36006  fvineqsneq  38429  indexdom  38762  filbcmb  38768  cdlemefr29exN  41553  rexanuz3  46205  reximdd  46257  disjrnmpt2  46297  disjinfi  46301  iunmapsn  46324  infnsuprnmpt  46356  rnmptbdlem  46361  supxrge  46444  suplesup  46445  infxr  46472  allbutfi  46498  supxrunb3  46504  infxrunb3rnmpt  46532  infrpgernmpt  46569  limsupre  46745  limsupub  46808  limsupre3lem  46836  limsupgtlem  46881  xlimmnfvlem1  46936  xlimpnfvlem1  46940  stoweidlem31  47135  stoweidlem34  47138  fourierdlem73  47283  sge0pnffigt  47500  sge0ltfirp  47504  sge0reuzb  47552  iundjiun  47564  ovnlerp  47666  smflimlem4  47878  smflimsuplem7  47930