Theorem 2eximi 1678

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

Syntax hints:   -> wi 4   E.wex 1633

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

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

This theorem is referenced by:  2mo  2324  2moOLD  2325  2eu6  2334  2eu6OLD  2335  cgsex2g  3092  cgsex4g  3093  vtocl2  3111  vtocl3  3112  dtru  4584  mosubopt  4687  elopaelxp  4895  xpdifid  5252  ssoprab2i  6371  hash1to3  12577  isfunc  15475  usgraop  24754  usgraedg4  24791  3v3e3cycl2  25068  frconngra  25425  bnj605  29279  bnj607  29288  bnj916  29305  bnj996  29327  bnj907  29337  bnj1128  29360  bj-dtru  30934  ac6s6f  31843  2uasbanh  36338  2uasbanhVD  36722