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

Theorem sylan9req 2442
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 2394 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2441 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649
This theorem is referenced by:  fndmu  5488  fodmrnu  5603  funcoeqres  5648  tz7.44-3  6604  dfac5lem4  7942  zdiv  10274  dvdsmulc  12806  smumullem  12933  mgmidmo  14622  reslmhm2b  16059  fclsfnflim  17982  ustuqtop1  18194  ulm2  20170  sineq0  20298  cxple2a  20459  sqff1o  20834  grpoidinvlem4  21645  hlimuni  22591  dmdsl3  23668  atoml2i  23736  disjpreima  23872  sspreima  23901  xrge0npcan  24047  fprodss  25055  eedimeq  25553  eqfnun  26116  ltrncnvnid  30243  cdleme20j  30434  cdleme42ke  30601  dia2dimlem13  31193  dvh4dimN  31564  mapdval4N  31749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2382
  Copyright terms: Public domain W3C validator