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  2652  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  spc2egv  3549  rexopabb  5471  relop  5795  elinxp  5973  opreuopreu  7972  en3  9171  en4  9172  addsrpr  10972  mulsrpr  10973  hash2prde  14383  hash3tpde  14406  pmtrrn2  19378  umgredg  29123  umgr2wlkon  29935  trsp2cyc  33099  acycgrsubgr  35209  satfvsucsuc  35416  fmla0xp  35434  fundmpss  35818  pellexlem5  42931  ax6e2eq  44655  fnchoice  45131  fzisoeu  45406  stoweidlem35  46138  stoweidlem60  46163  or2expropbi  47139  ich2exprop  47576  grlimprclnbgr  48101