Theorem 2eximi 1716

Description: Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

Hypothesis

Ref	Expression
eximi.1	|- ( ph -> ps )

Assertion

Ref	Expression
2eximi	|- ( E. x E. y ph -> E. x E. y ps )

Proof of Theorem 2eximi

Step	Hyp	Ref	Expression
1		eximi.1	. . 3 |- ( ph -> ps )
2	1	eximi 1715	. 2 |- ( E. y ph -> E. y ps )
3	2	eximi 1715	1 |- ( E. x E. y ph -> E. x E. y ps )

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

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

This theorem is referenced by:  2mo  2400  2eu6  2407  cgsex2g  3067  cgsex4g  3068  vtocl2  3088  vtocl3  3089  dtru  4592  mosubopt  4699  elopaelxp  4912  xpdifid  5271  ssoprab2i  6404  hash1to3  12689  isfunc  15847  usgraop  25156  usgraedg4  25193  3v3e3cycl2  25471  frconngra  25828  bnj605  29790  bnj607  29799  bnj916  29816  bnj996  29838  bnj907  29848  bnj1128  29871  bj-dtru  31478  ac6s6f  32480  2uasbanh  36998  2uasbanhVD  37371  umgr3v3e3cycl  40098