Theorem reximdai 3263

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

Syntax hints:   → wi 4  Ⅎwnf 1802   ∈ wcel 2141  ∀wral 3075  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-ral 3076  df-rex 3086

This theorem is referenced by:  2reurex  3721  fompt  7093  tz7.49  8409  hsmexlem2  10377  acunirnmpt2  32822  acunirnmpt2f  32823  locfinreflem  34097  cmpcref  34107  fvineqsneq  37866  indexdom  38193  filbcmb  38199  cdlemefr29exN  40986  rexanuz3  45634  reximdd  45686  disjrnmpt2  45726  disjinfi  45730  iunmapsn  45753  infnsuprnmpt  45785  rnmptbdlem  45790  supxrge  45874  suplesup  45875  infxr  45902  allbutfi  45928  supxrunb3  45934  infxrunb3rnmpt  45962  infrpgernmpt  45999  limsupre  46175  limsupub  46238  limsupre3lem  46266  limsupgtlem  46311  xlimmnfvlem1  46366  xlimpnfvlem1  46370  stoweidlem31  46565  stoweidlem34  46568  fourierdlem73  46713  sge0pnffigt  46930  sge0ltfirp  46934  sge0reuzb  46982  iundjiun  46994  ovnlerp  47096  smflimlem4  47308  smflimsuplem7  47360