Theorem 2eximdv 1922

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2eu6  2658  cgsex2g  3475  cgsex4g  3476  cgsex4gOLD  3477  spc2egv  3538  rexopabb  5441  relop  5759  elinxp  5929  opreuopreu  7876  en3  9054  en4  9055  addsrpr  10831  mulsrpr  10832  hash2prde  14184  pmtrrn2  19068  umgredg  27508  umgr2wlkon  28315  trsp2cyc  31390  acycgrsubgr  33120  satfvsucsuc  33327  fmla0xp  33345  fundmpss  33740  pellexlem5  40655  ax6e2eq  42177  fnchoice  42572  fzisoeu  42839  stoweidlem35  43576  stoweidlem60  43601  or2expropbi  44528  ich2exprop  44923