Theorem 2eximdv 1927

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1841. (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 1925	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
3	2	eximdv 1925	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-ex 1788

This theorem is referenced by:  2eu6  2657  cgsex2g  3441  cgsex4g  3442  cgsex4gOLD  3443  spc2egv  3504  rexopabb  5394  relop  5704  elinxp  5874  opreuopreu  7784  en3  8889  en4  8890  addsrpr  10654  mulsrpr  10655  hash2prde  14001  pmtrrn2  18806  umgredg  27183  umgr2wlkon  27988  trsp2cyc  31063  acycgrsubgr  32787  satfvsucsuc  32994  fmla0xp  33012  fundmpss  33410  pellexlem5  40299  ax6e2eq  41791  fnchoice  42186  fzisoeu  42453  stoweidlem35  43194  stoweidlem60  43219  or2expropbi  44143  ich2exprop  44539