Theorem 2eximdv 1717

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1659. (Contributed by NM, 3-Aug-1995.)

Hypothesis

Ref	Expression
2alimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
2eximdv	|- ( ph -> ( E. x E. y ps -> E. x E. y ch ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)   ch( x, y)

Proof of Theorem 2eximdv

Step	Hyp	Ref	Expression
1		2alimdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	eximdv 1715	. 2 |- ( ph -> ( E. y ps -> E. y ch ) )
3	2	eximdv 1715	1 |- ( ph -> ( E. x E. y ps -> E. x E. y ch ) )

Syntax hints:   -> wi 4   E.wex 1617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709

This theorem depends on definitions:  df-bi 185  df-ex 1618

This theorem is referenced by:  2eu6  2380  cgsex2g  3140  cgsex4g  3141  spc2egv  3193  spc3egv  3195  relop  5142  elres  5297  en3  7749  en4  7750  addsrpr  9441  mulsrpr  9442  hash2prde  12503  hash2prv  12512  hash2sspr  12513  pmtrrn2  16687  usgrarnedg  24589  fundmpss  29440  pellexlem5  31011  fnchoice  31647  fzisoeu  31742  stoweidlem35  32059  stoweidlem60  32084  usgedgimp  32794  usgedgimpALT  32797  ax6e2eq  33743