Theorem reximdai 3239

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

Syntax hints:   → wi 4  Ⅎwnf 1787   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-ral 3068  df-rex 3069

This theorem is referenced by:  2reurex  3690  tz7.49  8246  hsmexlem2  10114  acunirnmpt2  30899  acunirnmpt2f  30900  locfinreflem  31692  cmpcref  31702  fvineqsneq  35510  indexdom  35819  filbcmb  35825  cdlemefr29exN  38343  rexanuz3  42535  reximdd  42590  disjrnmpt2  42615  fompt  42619  disjinfi  42620  iunmapsn  42646  infnsuprnmpt  42685  rnmptbdlem  42690  supxrge  42767  suplesup  42768  infxr  42796  allbutfi  42823  supxrunb3  42829  infxrunb3rnmpt  42858  infrpgernmpt  42895  limsupre  43072  limsupub  43135  limsupre3lem  43163  limsupgtlem  43208  xlimmnfvlem1  43263  xlimpnfvlem1  43267  stoweidlem31  43462  stoweidlem34  43465  fourierdlem73  43610  sge0pnffigt  43824  sge0ltfirp  43828  sge0reuzb  43876  iundjiun  43888  ovnlerp  43990  smflimlem4  44196  smflimsuplem7  44246