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

Theorem sylan9req 2488
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 2440 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2487 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652
This theorem is referenced by:  fndmu  5538  fodmrnu  5653  funcoeqres  5698  tz7.44-3  6658  dfac5lem4  7997  zdiv  10330  dvdsmulc  12867  smumullem  12994  mgmidmo  14683  reslmhm2b  16120  fclsfnflim  18049  ustuqtop1  18261  ulm2  20291  sineq0  20419  cxple2a  20580  sqff1o  20955  grpoidinvlem4  21785  hlimuni  22731  dmdsl3  23808  atoml2i  23876  disjpreima  24016  sspreima  24047  xrge0npcan  24206  fprodss  25264  eedimeq  25802  eqfnun  26377  hashimarni  28106  sineq0ALT  28950  ltrncnvnid  30825  cdleme20j  31016  cdleme42ke  31183  dia2dimlem13  31775  dvh4dimN  32146  mapdval4N  32331
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator