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

Theorem syl5breqr 4161
Description: B chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
syl5breqr.1  |-  A R B
syl5breqr.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
syl5breqr  |-  ( ph  ->  A R C )

Proof of Theorem syl5breqr
StepHypRef Expression
1 syl5breqr.1 . 2  |-  A R B
2 syl5breqr.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2371 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5breq 4160 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647   class class class wbr 4125
This theorem is referenced by:  r1sdom  7593  alephordilem1  7847  mulge0  9438  xsubge0  10733  xmulgt0  10755  xmulge0  10756  xlemul1a  10760  sqlecan  11374  bernneq  11392  cnpart  11932  sqr0lem  11933  bitsfzo  12834  bitsmod  12835  bitsinv1lem  12840  pcge0  13122  prmreclem4  13174  prmreclem5  13175  isabvd  15795  abvtrivd  15815  nmolb2d  18440  nmoi  18450  nmoleub  18453  nmo0  18457  ovolge0  19055  itg1ge0a  19281  fta1g  19768  plyrem  19900  taylfval  19953  tayl0  19956  abelthlem2  20026  sinq12ge0  20094  relogrn  20137  logneg  20160  cxpge0  20252  amgmlem  20506  bposlem5  20750  lgsdir2lem2  20786  rpvmasumlem  20859  blocnilem  21695  pjssge0ii  22574  unierri  22997  esumcst  23920  eupath2lem3  24490  eupath2  24491  monotoddzzfi  26533  rmxypos  26540  rmygeid  26557  stoweidlem18  27273  frgrawopreglem2  27880
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126
  Copyright terms: Public domain W3C validator