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

Theorem syl5breqr 4483
Description: A 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 2475 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5breq 4482 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  r1sdom  8188  alephordilem1  8450  mulge0  10066  xsubge0  11449  xmulgt0  11471  xmulge0  11472  xlemul1a  11476  sqlecan  12236  bernneq  12254  hashge1  12419  hashge2el2dif  12481  cnpart  13030  sqr0lem  13031  bitsfzo  13937  bitsmod  13938  bitsinv1lem  13943  pcge0  14237  prmreclem4  14289  prmreclem5  14290  isabvd  17249  abvtrivd  17269  nmolb2d  20957  nmoi  20967  nmoleub  20970  nmo0  20974  ovolge0  21624  itg1ge0a  21850  fta1g  22300  plyrem  22432  taylfval  22485  abelthlem2  22558  sinq12ge0  22631  relogrn  22674  logneg  22697  cxpge0  22789  amgmlem  23044  bposlem5  23288  lgsdir2lem2  23324  rpvmasumlem  23397  eupath2lem3  24652  eupath2  24653  frgrawopreglem2  24719  blocnilem  25392  pjssge0ii  26273  unierri  26696  esumcst  27708  ballotlem5  28075  itgaddnclem2  29649  monotoddzzfi  30480  rmxypos  30487  rmygeid  30504  stoweidlem18  31318  stoweidlem55  31355  wallispi2lem1  31371  fourierdlem62  31469  fourierdlem104  31511  pgrpgt2nabl  32024  isnzr2hash  32027
  Copyright terms: Public domain W3C validator