Theorem 2eximdv 1906

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

Syntax hints:   -> wi 4   E.wex 1516

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2813  cgsex4g  2814  spc2egv  2870  spc3egv  2872  relop  4846  elres  5014  opabbrex  6012  th3q  6750  en2prde  7327  addnnnq0  7597  mulnnnq0  7598  prmuloc  7714  addsrpr  7893  mulsrpr  7894  upgrex  15814  umgredg  15849