Theorem reximdai 3270

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3083  df-rex 3093

This theorem is used by:  2reurex  3726  fompt  7120  tz7.49  8441  hsmexlem2  10429  acunirnmpt2  33042  acunirnmpt2f  33043  locfinreflem  34261  cmpcref  34271  fvineqsneq  38099  indexdom  38426  filbcmb  38432  cdlemefr29exN  41217  rexanuz3  45855  reximdd  45907  disjrnmpt2  45947  disjinfi  45951  iunmapsn  45974  infnsuprnmpt  46006  rnmptbdlem  46011  supxrge  46095  suplesup  46096  infxr  46123  allbutfi  46149  supxrunb3  46155  infxrunb3rnmpt  46183  infrpgernmpt  46220  limsupre  46396  limsupub  46459  limsupre3lem  46487  limsupgtlem  46532  xlimmnfvlem1  46587  xlimpnfvlem1  46591  stoweidlem31  46786  stoweidlem34  46789  fourierdlem73  46934  sge0pnffigt  47151  sge0ltfirp  47155  sge0reuzb  47203  iundjiun  47215  ovnlerp  47317  smflimlem4  47529  smflimsuplem7  47581