Theorem reximdai 3231

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3045  df-rex 3054

This theorem is referenced by:  2reurex  3722  fompt  7056  tz7.49  8374  hsmexlem2  10340  acunirnmpt2  32617  acunirnmpt2f  32618  locfinreflem  33806  cmpcref  33816  fvineqsneq  37385  indexdom  37713  filbcmb  37719  cdlemefr29exN  40381  rexanuz3  45074  reximdd  45126  disjrnmpt2  45166  disjinfi  45170  iunmapsn  45195  infnsuprnmpt  45228  rnmptbdlem  45233  supxrge  45318  suplesup  45319  infxr  45347  allbutfi  45373  supxrunb3  45379  infxrunb3rnmpt  45408  infrpgernmpt  45445  limsupre  45623  limsupub  45686  limsupre3lem  45714  limsupgtlem  45759  xlimmnfvlem1  45814  xlimpnfvlem1  45818  stoweidlem31  46013  stoweidlem34  46016  fourierdlem73  46161  sge0pnffigt  46378  sge0ltfirp  46382  sge0reuzb  46430  iundjiun  46442  ovnlerp  46544  smflimlem4  46756  smflimsuplem7  46808