Theorem 2eximi 1627

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

Syntax hints:   -> wi 4   E.wex 1587

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

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

This theorem is referenced by:  2mo  2369  2moOLD  2370  2eu6  2380  2eu6OLD  2381  cgsex2g  3112  cgsex4g  3113  vtocl2  3131  vtocl3  3132  dtru  4592  mosubopt  4698  xpdifid  5375  ssoprab2i  6290  isfunc  14894  usgraedg4  23458  3v3e3cycl2  23703  ac6s6f  29134  elopaelxp  30284  hash1to3  30384  frconngra  30762  2uasbanh  31603  2uasbanhVD  31980  bnj605  32233  bnj607  32242  bnj916  32259  bnj996  32281  bnj907  32291  bnj1128  32314  bj-dtru  32651