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  3554  rexopabb  5468  relop  5790  elinxp  5968  opreuopreu  7966  en3  9165  en4  9166  addsrpr  10966  mulsrpr  10967  hash2prde  14377  hash3tpde  14400  pmtrrn2  19373  umgredg  29117  umgr2wlkon  29929  trsp2cyc  33090  acycgrsubgr  35200  satfvsucsuc  35407  fmla0xp  35425  fundmpss  35809  pellexlem5  42872  ax6e2eq  44596  fnchoice  45072  fzisoeu  45347  stoweidlem35  46079  stoweidlem60  46104  or2expropbi  47071  ich2exprop  47508  grlimprclnbgr  48033