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

Theorem sylan9req 2457
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 2409 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2456 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  5505  fodmrnu  5620  funcoeqres  5665  tz7.44-3  6625  dfac5lem4  7963  zdiv  10296  dvdsmulc  12832  smumullem  12959  mgmidmo  14648  reslmhm2b  16085  fclsfnflim  18012  ustuqtop1  18224  ulm2  20254  sineq0  20382  cxple2a  20543  sqff1o  20918  grpoidinvlem4  21748  hlimuni  22694  dmdsl3  23771  atoml2i  23839  disjpreima  23979  sspreima  24010  xrge0npcan  24169  fprodss  25227  eedimeq  25741  eqfnun  26313  hashimarni  27995  ltrncnvnid  30609  cdleme20j  30800  cdleme42ke  30967  dia2dimlem13  31559  dvh4dimN  31930  mapdval4N  32115
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 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator