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

Theorem syl5eqbrr 4271
Description: B chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)
Hypotheses
Ref Expression
syl5eqbrr.1  |-  B  =  A
syl5eqbrr.2  |-  ( ph  ->  B R C )
Assertion
Ref Expression
syl5eqbrr  |-  ( ph  ->  A R C )

Proof of Theorem syl5eqbrr
StepHypRef Expression
1 syl5eqbrr.2 . 2  |-  ( ph  ->  B R C )
2 syl5eqbrr.1 . 2  |-  B  =  A
3 eqid 2442 . 2  |-  C  =  C
41, 2, 33brtr3g 4268 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   class class class wbr 4237
This theorem is referenced by:  enpr1g  7202  undom  7225  fidomdm  7417  prdom2  7921  infdif  8120  cfslb2n  8179  gchxpidm  8575  rankcf  8683  r1tskina  8688  tskuni  8689  ltsonq  8877  addgt0  9545  addgegt0  9546  addgtge0  9547  addge0  9548  expge1  11448  fsumrlim  12621  isumsup  12658  climcndslem1  12660  3dvds  12943  bitsinv1lem  12984  phicl2  13188  frgpnabllem1  15515  lt6abl  15535  pgpfaclem2  15671  unitmulcl  15800  xrsdsreclblem  16775  znidomb  16873  2ndcdisj2  17551  hmphindis  17860  metustexhalfOLD  18624  metustexhalf  18625  xrhmeo  19002  pcoass  19080  ovoliunlem1  19429  ismbl2  19454  voliunlem2  19476  ioombl1lem4  19486  itg2ge0  19656  itg2addlem  19679  itgge0  19731  dvfsumrlimge0  19945  abelthlem1  20378  abelthlem2  20379  pilem2  20399  rplogcl  20530  logge0  20531  argimgt0  20538  logdivlti  20546  logf1o2  20572  dvlog2lem  20574  ang180lem3  20684  atanlogaddlem  20784  atanlogsublem  20786  atantan  20794  atans2  20802  cxploglim2  20848  emcllem6  20870  emcllem7  20871  ftalem1  20886  ftalem2  20887  ppinncl  20988  chtrpcl  20989  vmalelog  21020  chtub  21027  logfacubnd  21036  logfacbnd3  21038  logfacrlim  21039  logexprlim  21040  mersenne  21042  perfectlem2  21045  bpos1lem  21097  bposlem1  21099  bposlem2  21100  bposlem3  21101  bposlem4  21102  bposlem5  21103  bposlem6  21104  lgseisen  21168  lgsquadlem1  21169  chebbnd1lem1  21194  chebbnd1lem3  21196  rpvmasumlem  21212  dchrvmasumlem2  21223  dchrvmasumlema  21225  dchrvmasumiflem1  21226  dchrisum0flblem2  21234  dchrisum0fno1  21236  dchrisum0re  21238  dirith2  21253  logdivsum  21258  mulog2sumlem1  21259  mulog2sumlem2  21260  log2sumbnd  21269  chpdifbndlem1  21278  chpdifbndlem2  21279  logdivbnd  21281  selberg3lem1  21282  pntpbnd1a  21310  pntpbnd2  21312  pntibndlem3  21317  pntlemn  21325  pntlemj  21328  pntlemk  21331  pnt  21339  minvecolem4  22413  dmct  24137  abrexct  24142  abrexctf  24144  xrge0addgt0  24245  esumcvg2  24508  lgamgulmlem2  24845  erdsze2lem2  24921  axlowdim  25931  pellqrex  26980  reglogltb  26992  reglogleb  26993  rmspecsqrnq  27007  rmspecnonsq  27008  rmspecpos  27017  lindfres  27308  fmul01  27724  stoweidlem26  27789  stoweidlem44  27807  stoweidlem45  27808  wallispilem3  27830  wallispi  27833  stirlinglem11  27847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-br 4238
  Copyright terms: Public domain W3C validator