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

Theorem 2eximi 1567
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 1566 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1566 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531
This theorem is referenced by:  excomim  1797  2eu6  2241  cgsex2g  2833  cgsex4g  2834  vtocl2  2852  vtocl3  2853  dtru  4217  mosubopt  4280  ssoprab2i  5952  isfunc  13754  3v3e3cycl2  28410  3v3e3cycl  28411  2uasbanh  28626  2uasbanhVD  29003  bnj605  29255  bnj607  29264  bnj916  29281  bnj996  29303  bnj907  29313  bnj1128  29336  excomimOLD7  29647
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator