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

Theorem sylan9req 2505
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 2451 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2504 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2435
This theorem is referenced by:  fndmu  5672  fodmrnu  5793  funcoeqres  5836  tz7.44-3  7076  dfac5lem4  8510  zdiv  10939  hashimarni  12476  ccatws1lenrev  12614  dvdsmulc  13888  smumullem  14019  mgmidmo  15760  reslmhm2b  17574  fclsfnflim  20401  ustuqtop1  20617  ulm2  22652  sineq0  22786  cxple2a  22952  sqff1o  23328  eedimeq  24073  grpoidinvlem4  25081  hlimuni  26028  dmdsl3  27106  atoml2i  27174  disjpreima  27317  sspreima  27357  xrge0npcan  27557  fprodss  29055  eqfnun  30187  cncfiooicc  31604  fourierdlem41  31819  fourierdlem71  31849  sineq0ALT  33470  ltrncnvnid  35591  cdleme20j  35784  cdleme42ke  35951  dia2dimlem13  36543  dvh4dimN  36914  mapdval4N  37099
  Copyright terms: Public domain W3C validator