MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2eximi Structured version   Unicode version

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
StepHypRef Expression
1 eximi.1 . . 3  |-  ( ph  ->  ps )
21eximi 1626 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1626 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator