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

Theorem syl5eqbrr 4057
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 2283 . 2  |-  C  =  C
41, 2, 33brtr3g 4054 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  enpr1g  6927  undom  6950  fidomdm  7138  prdom2  7636  infdif  7835  cfslb2n  7894  gchxpidm  8291  rankcf  8399  r1tskina  8404  tskuni  8405  ltsonq  8593  addgt0  9260  addgegt0  9261  addgtge0  9262  addge0  9263  expge1  11139  fsumrlim  12269  isumsup  12306  climcndslem1  12308  3dvds  12591  bitsinv1lem  12632  phicl2  12836  frgpnabllem1  15161  lt6abl  15181  pgpfaclem2  15317  unitmulcl  15446  xrsdsreclblem  16417  znidomb  16515  2ndcdisj2  17183  hmphindis  17488  xrhmeo  18444  pcoass  18522  ovoliunlem1  18861  ismbl2  18886  voliunlem2  18908  ioombl1lem4  18918  itg2ge0  19090  itg2addlem  19113  itgge0  19165  dvfsumrlimge0  19377  abelthlem1  19807  abelthlem2  19808  pilem2  19828  rplogcl  19958  logge0  19959  argimgt0  19966  logdivlti  19971  logf1o2  19997  dvlog2lem  19999  ang180lem3  20109  atanlogaddlem  20209  atanlogsublem  20211  atantan  20219  atans2  20227  cxploglim2  20273  emcllem6  20294  emcllem7  20295  ftalem1  20310  ftalem2  20311  ppinncl  20412  chtrpcl  20413  vmalelog  20444  chtub  20451  logfacubnd  20460  logfacbnd3  20462  logfacrlim  20463  logexprlim  20464  mersenne  20466  perfectlem2  20469  bpos1lem  20521  bposlem1  20523  bposlem2  20524  bposlem3  20525  bposlem4  20526  bposlem5  20527  bposlem6  20528  lgseisen  20592  lgsquadlem1  20593  chebbnd1lem1  20618  chebbnd1lem3  20620  rpvmasumlem  20636  dchrvmasumlem2  20647  dchrvmasumlema  20649  dchrvmasumiflem1  20650  dchrisum0flblem2  20658  dchrisum0fno1  20660  dchrisum0re  20662  dirith2  20677  logdivsum  20682  mulog2sumlem1  20683  mulog2sumlem2  20684  log2sumbnd  20693  chpdifbndlem1  20702  chpdifbndlem2  20703  logdivbnd  20705  selberg3lem1  20706  pntpbnd1a  20734  pntpbnd2  20736  pntibndlem3  20741  pntlemn  20749  pntlemj  20752  pntlemk  20755  pnt  20763  minvecolem4  21459  esumcvg2  23455  erdsze2lem2  23735  axlowdim  24589  pellqrex  26964  reglogltb  26976  reglogleb  26977  rmspecsqrnq  26991  rmspecnonsq  26992  rmspecpos  27001  lindfres  27293  fmul01  27710  stoweidlem26  27775  stoweidlem44  27793  stoweidlem45  27794  wallispilem3  27816  wallispi  27819
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator