Theorem reximdai 3253

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

Syntax hints:   → wi 4  Ⅎwnf 1778   ∈ wcel 2099  ∀wral 3056  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2164

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-nf 1779  df-ral 3057  df-rex 3066

This theorem is referenced by:  2reurex  3753  fompt  7122  tz7.49  8459  hsmexlem2  10444  acunirnmpt2  32439  acunirnmpt2f  32440  locfinreflem  33431  cmpcref  33441  fvineqsneq  36881  indexdom  37196  filbcmb  37202  cdlemefr29exN  39864  rexanuz3  44434  reximdd  44490  disjrnmpt2  44533  disjinfi  44537  iunmapsn  44562  infnsuprnmpt  44598  rnmptbdlem  44603  supxrge  44692  suplesup  44693  infxr  44721  allbutfi  44747  supxrunb3  44753  infxrunb3rnmpt  44782  infrpgernmpt  44819  limsupre  45001  limsupub  45064  limsupre3lem  45092  limsupgtlem  45137  xlimmnfvlem1  45192  xlimpnfvlem1  45196  stoweidlem31  45391  stoweidlem34  45394  fourierdlem73  45539  sge0pnffigt  45756  sge0ltfirp  45760  sge0reuzb  45808  iundjiun  45820  ovnlerp  45922  smflimlem4  46134  smflimsuplem7  46186