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  2657  cgsex2g  3486  cgsex4g  3487  cgsex4gOLD  3488  spc2egv  3553  rexopabb  5476  relop  5799  elinxp  5978  opreuopreu  7978  en3  9181  en4  9182  addsrpr  10986  mulsrpr  10987  hash2prde  14393  hash3tpde  14416  pmtrrn2  19389  umgredg  29211  umgr2wlkon  30023  trsp2cyc  33205  acycgrsubgr  35352  satfvsucsuc  35559  fmla0xp  35577  fundmpss  35961  pellexlem5  43071  ax6e2eq  44794  fnchoice  45270  fzisoeu  45544  stoweidlem35  46275  stoweidlem60  46300  or2expropbi  47276  ich2exprop  47713  grlimprclnbgr  48238