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

Theorem sylan9req 2349
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 2301 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2348 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632
This theorem is referenced by:  fndmu  5361  fodmrnu  5475  funcoeqres  5520  tz7.44-3  6437  dfac5lem4  7769  zdiv  10098  dvdsmulc  12572  smumullem  12699  mgmidmo  14386  reslmhm2b  15827  fclsfnflim  17738  ulm2  19780  sineq0  19905  cxple2a  20062  sqff1o  20436  grpoidinvlem4  20890  hlimuni  21834  dmdsl3  22911  atoml2i  22979  sspreima  23225  eedimeq  24598  eqfnun  26490  ltrncnvnid  30938  cdleme20j  31129  cdleme42ke  31296  dia2dimlem13  31888  dvh4dimN  32259  mapdval4N  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator