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

Theorem 2eximi 1587
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 1586 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1586 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1551
This theorem is referenced by:  excomimOLD  1882  2eu6  2368  cgsex2g  2990  cgsex4g  2991  vtocl2  3009  vtocl3  3010  dtru  4392  mosubopt  4456  ssoprab2i  6164  isfunc  14063  usgraedg4  21408  3v3e3cycl2  21653  elopaelxp  28073  frconngra  28473  2uasbanh  28710  2uasbanhVD  29085  bnj605  29340  bnj607  29349  bnj916  29366  bnj996  29388  bnj907  29398  bnj1128  29421  excomimOLD7  29755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator