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

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