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

Theorem sylan9req 2494
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 2446 . 2  |-  ( ph  ->  A  =  B )
3 sylan9req.2 . 2  |-  ( ps 
->  B  =  C
)
42, 3sylan9eq 2493 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2434
This theorem is referenced by:  fndmu  5509  fodmrnu  5625  funcoeqres  5668  tz7.44-3  6860  dfac5lem4  8292  zdiv  10708  hashimarni  12197  ccatws1lenrev  12305  dvdsmulc  13556  smumullem  13684  mgmidmo  15414  reslmhm2b  17113  fclsfnflim  19559  ustuqtop1  19775  ulm2  21809  sineq0  21942  cxple2a  22103  sqff1o  22479  eedimeq  23079  grpoidinvlem4  23629  hlimuni  24576  dmdsl3  25654  atoml2i  25722  disjpreima  25863  sspreima  25897  xrge0npcan  26090  fprodss  27390  eqfnun  28540  sineq0ALT  31507  ltrncnvnid  33493  cdleme20j  33684  cdleme42ke  33851  dia2dimlem13  34443  dvh4dimN  34814  mapdval4N  34999
  Copyright terms: Public domain W3C validator