Theorem 2eximdv 1930

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 1928	. 2 |- ( ph -> ( E. y ps -> E. y ch ) )
3	2	eximdv 1928	1 |- ( ph -> ( E. x E. y ps -> E. x E. y ch ) )

Syntax hints:   -> wi 4   E.wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2839  cgsex4g  2840  spc2egv  2896  spc3egv  2898  relop  4880  elres  5049  opabbrex  6064  th3q  6808  en2prde  7397  addnnnq0  7668  mulnnnq0  7669  prmuloc  7785  addsrpr  7964  mulsrpr  7965  upgrex  15953  umgredg  15995