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

Theorem sylan9req 2513
Description: An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
Hypotheses
Ref Expression
sylan9req.1  |-  ( ph  ->  B  =  A )
sylan9req.2  |-  ( ps 
->  B  =  C
)
Assertion
Ref Expression
sylan9req  |-  ( (
ph  /\  ps )  ->  A  =  C )

Proof of Theorem sylan9req
StepHypRef Expression
1 sylan9req.1 . . 3  |-  ( ph  ->  B  =  A )
21eqcomd 2459 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2512 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2443
This theorem is referenced by:  fndmu  5610  fodmrnu  5726  funcoeqres  5769  tz7.44-3  6964  dfac5lem4  8397  zdiv  10813  hashimarni  12303  ccatws1lenrev  12411  dvdsmulc  13662  smumullem  13790  mgmidmo  15520  reslmhm2b  17241  fclsfnflim  19716  ustuqtop1  19932  ulm2  21966  sineq0  22099  cxple2a  22260  sqff1o  22636  eedimeq  23279  grpoidinvlem4  23829  hlimuni  24776  dmdsl3  25854  atoml2i  25922  disjpreima  26062  sspreima  26096  xrge0npcan  26291  fprodss  27595  eqfnun  28753  sineq0ALT  31973  ltrncnvnid  34077  cdleme20j  34268  cdleme42ke  34435  dia2dimlem13  35027  dvh4dimN  35398  mapdval4N  35583
  Copyright terms: Public domain W3C validator