Theorem reximdai 3244

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

Syntax hints:   → wi 4  Ⅎwnf 1786   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 1783  df-nf 1787  df-ral 3069  df-rex 3070

This theorem is referenced by:  2reurex  3695  tz7.49  8276  hsmexlem2  10183  acunirnmpt2  30997  acunirnmpt2f  30998  locfinreflem  31790  cmpcref  31800  fvineqsneq  35583  indexdom  35892  filbcmb  35898  cdlemefr29exN  38416  rexanuz3  42646  reximdd  42701  disjrnmpt2  42726  fompt  42730  disjinfi  42731  iunmapsn  42757  infnsuprnmpt  42796  rnmptbdlem  42801  supxrge  42877  suplesup  42878  infxr  42906  allbutfi  42933  supxrunb3  42939  infxrunb3rnmpt  42968  infrpgernmpt  43005  limsupre  43182  limsupub  43245  limsupre3lem  43273  limsupgtlem  43318  xlimmnfvlem1  43373  xlimpnfvlem1  43377  stoweidlem31  43572  stoweidlem34  43575  fourierdlem73  43720  sge0pnffigt  43934  sge0ltfirp  43938  sge0reuzb  43986  iundjiun  43998  ovnlerp  44100  smflimlem4  44309  smflimsuplem7  44359