Theorem 2eximdv 1774

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

Syntax hints:   -> wi 4   E.wex 1671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-ex 1672

This theorem is referenced by:  2eu6  2407  cgsex2g  3067  cgsex4g  3068  spc2egv  3122  spc3egv  3124  relop  4990  elres  5146  en3  7826  en4  7827  addsrpr  9517  mulsrpr  9518  hash2prde  12672  pmtrrn2  17179  usgrarnedg  25190  fundmpss  30478  pellexlem5  35748  ax6e2eq  36994  fnchoice  37413  fzisoeu  37606  stoweidlem35  38008  stoweidlem60  38033  umgredg  39390  umgr2wlkon  40072  usgedgimp  40223  usgedgimpALT  40226