Theorem reximdai 3267

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

Syntax hints:   → wi 4  Ⅎwnf 1813   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-ral 3080  df-rex 3090

This theorem is referenced by:  2reurex  3724  fompt  7115  tz7.49  8433  hsmexlem2  10412  acunirnmpt2  32986  acunirnmpt2f  32987  locfinreflem  34211  cmpcref  34221  fvineqsneq  38039  indexdom  38366  filbcmb  38372  cdlemefr29exN  41157  rexanuz3  45797  reximdd  45849  disjrnmpt2  45889  disjinfi  45893  iunmapsn  45916  infnsuprnmpt  45948  rnmptbdlem  45953  supxrge  46037  suplesup  46038  infxr  46065  allbutfi  46091  supxrunb3  46097  infxrunb3rnmpt  46125  infrpgernmpt  46162  limsupre  46338  limsupub  46401  limsupre3lem  46429  limsupgtlem  46474  xlimmnfvlem1  46529  xlimpnfvlem1  46533  stoweidlem31  46728  stoweidlem34  46731  fourierdlem73  46876  sge0pnffigt  47093  sge0ltfirp  47097  sge0reuzb  47145  iundjiun  47157  ovnlerp  47259  smflimlem4  47471  smflimsuplem7  47523