Theorem 2eximdv 1920

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  2eu6  2654  cgsex2g  3483  cgsex4g  3484  cgsex4gOLD  3485  spc2egv  3550  rexopabb  5471  relop  5794  elinxp  5972  opreuopreu  7972  en3  9172  en4  9173  addsrpr  10973  mulsrpr  10974  hash2prde  14379  hash3tpde  14402  pmtrrn2  19374  umgredg  29118  umgr2wlkon  29930  trsp2cyc  33099  acycgrsubgr  35223  satfvsucsuc  35430  fmla0xp  35448  fundmpss  35832  pellexlem5  42951  ax6e2eq  44675  fnchoice  45151  fzisoeu  45426  stoweidlem35  46158  stoweidlem60  46183  or2expropbi  47159  ich2exprop  47596  grlimprclnbgr  48121