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

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