Theorem reximdai 3041

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

Syntax hints:   → wi 4  Ⅎwnf 1748   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750  df-ral 2946  df-rex 2947

This theorem is referenced by:  tz7.49  7585  hsmexlem2  9287  acunirnmpt2  29588  acunirnmpt2f  29589  locfinreflem  30035  cmpcref  30045  indexdom  33659  filbcmb  33665  cdlemefr29exN  36007  rexanuz3  39589  reximdd  39658  disjrnmpt2  39689  fompt  39693  disjinfi  39694  iunmapsn  39723  infnsuprnmpt  39779  rnmptbdlem  39784  supxrge  39867  suplesup  39868  infxr  39896  allbutfi  39929  supxrunb3  39936  infxrunb3rnmpt  39968  infrpgernmpt  40008  limsupre  40191  limsupub  40254  limsupre3lem  40282  limsupgtlem  40327  xlimmnfvlem1  40376  xlimpnfvlem1  40380  stoweidlem31  40566  stoweidlem34  40569  fourierdlem73  40714  sge0pnffigt  40931  sge0ltfirp  40935  sge0reuzb  40983  iundjiun  40995  ovnlerp  41097  smflimlem4  41303  smflimsuplem7  41353  2reurex  41502