Theorem 2eximdv 1938

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

Syntax hints:   → wi 4  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  2eu6  2682  cgsex2g  3498  cgsex4g  3499  spc2egv  3558  rexopabb  5497  relop  5820  elinxp  6003  opreuopreu  8011  en3  9221  en4  9222  addsrpr  11030  mulsrpr  11031  hash2prde  14480  hash3tpde  14503  pmtrrn2  19483  umgredg  29285  umgr2wlkon  30096  trsp2cyc  33264  acycgrsubgr  35472  satfvsucsuc  35679  fmla0xp  35697  fundmpss  36081  cgsex2gd  37593  pellexlem5  43374  ax6e2eq  45097  fnchoice  45573  fzisoeu  45843  stoweidlem35  46573  stoweidlem60  46598  or2expropbi  47592  ich2exprop  48041  grlimprclnbgr  48582