Theorem 2eximdv 1921

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1836. (Contributed by NM, 3-Aug-1995.)

Hypothesis

Ref	Expression
2alimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
2eximdv	⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem 2eximdv

Step	Hyp	Ref	Expression
1		2alimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	eximdv 1919	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
3	2	eximdv 1919	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4  ∃wex 1781

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 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  2eu6  2657  cgsex2g  3475  cgsex4g  3476  spc2egv  3541  rexopabb  5483  relop  5805  elinxp  5984  opreuopreu  7987  en3  9191  en4  9192  addsrpr  10998  mulsrpr  10999  hash2prde  14432  hash3tpde  14455  pmtrrn2  19435  umgredg  29207  umgr2wlkon  30018  trsp2cyc  33184  acycgrsubgr  35340  satfvsucsuc  35547  fmla0xp  35565  fundmpss  35949  cgsex2gd  37451  pellexlem5  43261  ax6e2eq  44984  fnchoice  45460  fzisoeu  45733  stoweidlem35  46463  stoweidlem60  46488  or2expropbi  47482  ich2exprop  47931  grlimprclnbgr  48472