Theorem reximdai 3268

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3081  df-rex 3091

This theorem is used by:  2reurex  3721  fompt  7145  tz7.49  8486  hsmexlem2  10535  acunirnmpt2  33329  acunirnmpt2f  33330  locfinreflem  34555  cmpcref  34565  srepdflem2  36099  fvineqsneq  38540  indexdom  38873  filbcmb  38877  cdlemefr29exN  41662  rexanuz3  46326  reximdd  46378  disjrnmpt2  46418  disjinfi  46422  iunmapsn  46445  infnsuprnmpt  46477  rnmptbdlem  46482  supxrge  46565  suplesup  46566  infxr  46593  allbutfi  46619  supxrunb3  46625  infxrunb3rnmpt  46653  infrpgernmpt  46690  limsupre  46866  limsupub  46929  limsupre3lem  46957  limsupgtlem  47002  xlimmnfvlem1  47057  xlimpnfvlem1  47061  stoweidlem31  47256  stoweidlem34  47259  fourierdlem73  47404  sge0pnffigt  47621  sge0ltfirp  47625  sge0reuzb  47673  iundjiun  47685  ovnlerp  47787  smflimlem4  47999  smflimsuplem7  48051