Theorem 2eximi 1708

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

Syntax hints:   -> wi 4   E.wex 1663

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

This theorem depends on definitions:  df-bi 189  df-ex 1664

This theorem is referenced by:  2mo  2380  2eu6  2387  cgsex2g  3081  cgsex4g  3082  vtocl2  3102  vtocl3  3103  dtru  4594  mosubopt  4699  elopaelxp  4907  xpdifid  5265  ssoprab2i  6385  hash1to3  12648  isfunc  15769  usgraop  25077  usgraedg4  25114  3v3e3cycl2  25392  frconngra  25749  bnj605  29718  bnj607  29727  bnj916  29744  bnj996  29766  bnj907  29776  bnj1128  29799  bj-dtru  31412  ac6s6f  32416  2uasbanh  36928  2uasbanhVD  37308