Theorem reximdai 3266

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088

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 1943  ax-6 2000  ax-7 2041  ax-12 2215

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

This theorem is used by:  2reurex  3721  fompt  7115  tz7.49  8438  hsmexlem2  10433  acunirnmpt2  33141  acunirnmpt2f  33142  locfinreflem  34358  cmpcref  34368  fvineqsneq  38174  indexdom  38492  filbcmb  38498  cdlemefr29exN  41283  rexanuz3  45936  reximdd  45988  disjrnmpt2  46028  disjinfi  46032  iunmapsn  46055  infnsuprnmpt  46087  rnmptbdlem  46092  supxrge  46176  suplesup  46177  infxr  46204  allbutfi  46230  supxrunb3  46236  infxrunb3rnmpt  46264  infrpgernmpt  46301  limsupre  46477  limsupub  46540  limsupre3lem  46568  limsupgtlem  46613  xlimmnfvlem1  46668  xlimpnfvlem1  46672  stoweidlem31  46867  stoweidlem34  46870  fourierdlem73  47015  sge0pnffigt  47232  sge0ltfirp  47236  sge0reuzb  47284  iundjiun  47296  ovnlerp  47398  smflimlem4  47610  smflimsuplem7  47662