Theorem reximdai 3254

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

Syntax hints:   → wi 4  Ⅎwnf 1746   ∈ wcel 2050  ∀wral 3088  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-nf 1747  df-ral 3093  df-rex 3094

This theorem is referenced by:  2reurex  3661  tz7.49  7886  hsmexlem2  9649  acunirnmpt2  30170  acunirnmpt2f  30171  locfinreflem  30748  cmpcref  30758  fvineqsneq  34134  indexdom  34451  filbcmb  34457  cdlemefr29exN  36983  rexanuz3  40785  reximdd  40844  disjrnmpt2  40874  fompt  40878  disjinfi  40879  iunmapsn  40906  infnsuprnmpt  40951  rnmptbdlem  40956  supxrge  41036  suplesup  41037  infxr  41065  allbutfi  41096  supxrunb3  41103  infxrunb3rnmpt  41134  infrpgernmpt  41173  limsupre  41354  limsupub  41417  limsupre3lem  41445  limsupgtlem  41490  xlimmnfvlem1  41545  xlimpnfvlem1  41549  stoweidlem31  41748  stoweidlem34  41751  fourierdlem73  41896  sge0pnffigt  42110  sge0ltfirp  42114  sge0reuzb  42162  iundjiun  42174  ovnlerp  42276  smflimlem4  42482  smflimsuplem7  42532