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

Theorem sylan9req 2524
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 2470 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2523 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2454
This theorem is referenced by:  fndmu  5675  fodmrnu  5796  funcoeqres  5839  tz7.44-3  7066  dfac5lem4  8498  zdiv  10922  hashimarni  12452  ccatws1lenrev  12587  dvdsmulc  13863  smumullem  13992  mgmidmo  15726  reslmhm2b  17478  fclsfnflim  20258  ustuqtop1  20474  ulm2  22509  sineq0  22642  cxple2a  22803  sqff1o  23179  eedimeq  23872  grpoidinvlem4  24873  hlimuni  25820  dmdsl3  26898  atoml2i  26966  disjpreima  27106  sspreima  27145  xrge0npcan  27334  fprodss  28645  eqfnun  29804  sineq0ALT  32694  ltrncnvnid  34800  cdleme20j  34991  cdleme42ke  35158  dia2dimlem13  35750  dvh4dimN  36121  mapdval4N  36306
  Copyright terms: Public domain W3C validator