Theorem reximdai 3235

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3049  df-rex 3058

This theorem is referenced by:  2reurex  3715  fompt  7059  tz7.49  8372  hsmexlem2  10327  acunirnmpt2  32646  acunirnmpt2f  32647  locfinreflem  33876  cmpcref  33886  fvineqsneq  37479  indexdom  37797  filbcmb  37803  cdlemefr29exN  40524  rexanuz3  45220  reximdd  45272  disjrnmpt2  45312  disjinfi  45316  iunmapsn  45341  infnsuprnmpt  45374  rnmptbdlem  45379  supxrge  45464  suplesup  45465  infxr  45492  allbutfi  45518  supxrunb3  45524  infxrunb3rnmpt  45553  infrpgernmpt  45590  limsupre  45766  limsupub  45829  limsupre3lem  45857  limsupgtlem  45902  xlimmnfvlem1  45957  xlimpnfvlem1  45961  stoweidlem31  46156  stoweidlem34  46159  fourierdlem73  46304  sge0pnffigt  46521  sge0ltfirp  46525  sge0reuzb  46573  iundjiun  46585  ovnlerp  46687  smflimlem4  46899  smflimsuplem7  46951