Theorem reximdai 3012

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

Syntax hints:   → wi 4  Ⅎwnf 1708   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710  df-ral 2917  df-rex 2918

This theorem is referenced by:  tz7.49  7540  hsmexlem2  9249  acunirnmpt2  29460  acunirnmpt2f  29461  locfinreflem  29907  cmpcref  29917  indexdom  33529  filbcmb  33535  cdlemefr29exN  35690  rexanuz3  39275  reximdd  39344  disjrnmpt2  39375  fompt  39379  disjinfi  39380  iunmapsn  39409  infnsuprnmpt  39465  rnmptbdlem  39470  supxrge  39554  suplesup  39555  infxr  39583  allbutfi  39616  supxrunb3  39623  infxrunb3rnmpt  39655  infrpgernmpt  39695  limsupre  39873  limsupub  39936  limsupre3lem  39964  limsupgtlem  40009  xlimmnfvlem1  40058  xlimpnfvlem1  40062  stoweidlem31  40248  stoweidlem34  40251  fourierdlem73  40396  sge0pnffigt  40613  sge0ltfirp  40617  sge0reuzb  40665  iundjiun  40677  ovnlerp  40776  smflimlem4  40982  smflimsuplem7  41032  2reurex  41181