Theorem reximdai 3270

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3111  df-rex 3112

This theorem is referenced by:  2reurex  3698  tz7.49  8064  hsmexlem2  9838  acunirnmpt2  30423  acunirnmpt2f  30424  locfinreflem  31193  cmpcref  31203  fvineqsneq  34829  indexdom  35172  filbcmb  35178  cdlemefr29exN  37698  rexanuz3  41732  reximdd  41789  disjrnmpt2  41815  fompt  41819  disjinfi  41820  iunmapsn  41846  infnsuprnmpt  41888  rnmptbdlem  41893  supxrge  41970  suplesup  41971  infxr  41999  allbutfi  42029  supxrunb3  42036  infxrunb3rnmpt  42065  infrpgernmpt  42104  limsupre  42283  limsupub  42346  limsupre3lem  42374  limsupgtlem  42419  xlimmnfvlem1  42474  xlimpnfvlem1  42478  stoweidlem31  42673  stoweidlem34  42676  fourierdlem73  42821  sge0pnffigt  43035  sge0ltfirp  43039  sge0reuzb  43087  iundjiun  43099  ovnlerp  43201  smflimlem4  43407  smflimsuplem7  43457