Theorem 2eximdv 1918

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

Syntax hints:   → wi 4  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  2eu6  2660  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  spc2egv  3612  rexopabb  5547  relop  5875  elinxp  6048  opreuopreu  8075  en3  9344  en4  9345  addsrpr  11144  mulsrpr  11145  hash2prde  14519  hash3tpde  14542  pmtrrn2  19502  umgredg  29173  umgr2wlkon  29983  trsp2cyc  33116  acycgrsubgr  35126  satfvsucsuc  35333  fmla0xp  35351  fundmpss  35730  pellexlem5  42789  ax6e2eq  44528  fnchoice  44929  fzisoeu  45215  stoweidlem35  45956  stoweidlem60  45981  or2expropbi  46949  ich2exprop  47345