Theorem 2eximdv 1756

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1701. (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 1754	. 2 |- ( ph -> ( E. y ps -> E. y ch ) )
3	2	eximdv 1754	1 |- ( ph -> ( E. x E. y ps -> E. x E. y ch ) )

Syntax hints:   -> wi 4   E.wex 1659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-ex 1660

This theorem is referenced by:  2eu6  2356  cgsex2g  3115  cgsex4g  3116  spc2egv  3168  spc3egv  3170  relop  5001  elres  5156  en3  7811  en4  7812  addsrpr  9500  mulsrpr  9501  hash2prde  12629  hash2prv  12640  hash2sspr  12641  pmtrrn2  17089  usgrarnedg  25098  fundmpss  30402  pellexlem5  35597  ax6e2eq  36782  fnchoice  37211  fzisoeu  37360  stoweidlem35  37716  stoweidlem60  37741  usgrrnedg  38917  usgedgimp  38987  usgedgimpALT  38990