Theorem 2eximi 1631

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 1630	. 2 |- ( E. y ph -> E. y ps )
3	2	eximi 1630	1 |- ( E. x E. y ph -> E. x E. y ps )

Syntax hints:   -> wi 4   E.wex 1591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607

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

This theorem is referenced by:  2mo  2375  2moOLD  2376  2eu6  2386  2eu6OLD  2387  cgsex2g  3140  cgsex4g  3141  vtocl2  3159  vtocl3  3160  dtru  4631  mosubopt  4738  elopaelxp  5064  xpdifid  5426  ssoprab2i  6366  hash1to3  12483  isfunc  15080  usgraop  24013  usgraedg4  24049  3v3e3cycl2  24326  frconngra  24683  ac6s6f  30172  2uasbanh  32289  2uasbanhVD  32666  bnj605  32919  bnj607  32928  bnj916  32945  bnj996  32967  bnj907  32977  bnj1128  33000  bj-dtru  33339