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

Theorem 2eximi 1564
Description: Inference adding 2 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 1563 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1563 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  excomim  1785  2eu6  2228  cgsex2g  2820  cgsex4g  2821  vtocl2  2839  vtocl3  2840  dtru  4201  mosubopt  4264  ssoprab2i  5936  isfunc  13738  2uasbanh  28327  2uasbanhVD  28687  bnj605  28939  bnj607  28948  bnj916  28965  bnj996  28987  bnj907  28997  bnj1128  29020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator