Theorem reximdai 3239

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3045  df-rex 3054

This theorem is referenced by:  2reurex  3731  fompt  7090  tz7.49  8413  hsmexlem2  10380  acunirnmpt2  32584  acunirnmpt2f  32585  locfinreflem  33830  cmpcref  33840  fvineqsneq  37400  indexdom  37728  filbcmb  37734  cdlemefr29exN  40396  rexanuz3  45090  reximdd  45142  disjrnmpt2  45182  disjinfi  45186  iunmapsn  45211  infnsuprnmpt  45244  rnmptbdlem  45249  supxrge  45334  suplesup  45335  infxr  45363  allbutfi  45389  supxrunb3  45395  infxrunb3rnmpt  45424  infrpgernmpt  45461  limsupre  45639  limsupub  45702  limsupre3lem  45730  limsupgtlem  45775  xlimmnfvlem1  45830  xlimpnfvlem1  45834  stoweidlem31  46029  stoweidlem34  46032  fourierdlem73  46177  sge0pnffigt  46394  sge0ltfirp  46398  sge0reuzb  46446  iundjiun  46458  ovnlerp  46560  smflimlem4  46772  smflimsuplem7  46824