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

Theorem sylan9req 2336
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 2288 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2335 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623
This theorem is referenced by:  fndmu  5345  fodmrnu  5459  funcoeqres  5504  tz7.44-3  6421  dfac5lem4  7753  zdiv  10082  dvdsmulc  12556  smumullem  12683  mgmidmo  14370  reslmhm2b  15811  fclsfnflim  17722  ulm2  19764  sineq0  19889  cxple2a  20046  sqff1o  20420  grpoidinvlem4  20874  hlimuni  21818  dmdsl3  22895  atoml2i  22963  sspreima  23210  eedimeq  24526  eqfnun  26387  ltrncnvnid  30316  cdleme20j  30507  cdleme42ke  30674  dia2dimlem13  31266  dvh4dimN  31637  mapdval4N  31822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator