Theorem 2eximdv 1679

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (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 1677	. 2 |- ( ph -> ( E. y ps -> E. y ch ) )
3	2	eximdv 1677	1 |- ( ph -> ( E. x E. y ps -> E. x E. y ch ) )

Syntax hints:   -> wi 4   E.wex 1587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671

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

This theorem is referenced by:  2eu6  2380  cgsex2g  3112  cgsex4g  3113  spc2egv  3165  spc3egv  3167  relop  5099  elres  5254  th3q  7320  en3  7661  en4  7662  hash2prde  12298  pmtrrn2  16086  usgrarnedg  23456  fundmpss  27722  pellexlem5  29323  fnchoice  29900  stoweidlem35  29979  stoweidlem60  30004  hash2prv  30375  hash2sspr  30376  ax6e2eq  31599