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

Theorem 2eximi 1716
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 1715 . 2  |-  ( E. y ph  ->  E. y ps )
32eximi 1715 1  |-  ( E. x E. y ph  ->  E. x E. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  2mo  2400  2eu6  2407  cgsex2g  3067  cgsex4g  3068  vtocl2  3088  vtocl3  3089  dtru  4592  mosubopt  4699  elopaelxp  4912  xpdifid  5271  ssoprab2i  6404  hash1to3  12689  isfunc  15847  usgraop  25156  usgraedg4  25193  3v3e3cycl2  25471  frconngra  25828  bnj605  29790  bnj607  29799  bnj916  29816  bnj996  29838  bnj907  29848  bnj1128  29871  bj-dtru  31478  ac6s6f  32480  2uasbanh  36998  2uasbanhVD  37371  umgr3v3e3cycl  40098
  Copyright terms: Public domain W3C validator