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

Theorem syl5eqbrr 4073
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 2296 . 2  |-  C  =  C
41, 2, 33brtr3g 4070 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  enpr1g  6943  undom  6966  fidomdm  7154  prdom2  7652  infdif  7851  cfslb2n  7910  gchxpidm  8307  rankcf  8415  r1tskina  8420  tskuni  8421  ltsonq  8609  addgt0  9276  addgegt0  9277  addgtge0  9278  addge0  9279  expge1  11155  fsumrlim  12285  isumsup  12322  climcndslem1  12324  3dvds  12607  bitsinv1lem  12648  phicl2  12852  frgpnabllem1  15177  lt6abl  15197  pgpfaclem2  15333  unitmulcl  15462  xrsdsreclblem  16433  znidomb  16531  2ndcdisj2  17199  hmphindis  17504  xrhmeo  18460  pcoass  18538  ovoliunlem1  18877  ismbl2  18902  voliunlem2  18924  ioombl1lem4  18934  itg2ge0  19106  itg2addlem  19129  itgge0  19181  dvfsumrlimge0  19393  abelthlem1  19823  abelthlem2  19824  pilem2  19844  rplogcl  19974  logge0  19975  argimgt0  19982  logdivlti  19987  logf1o2  20013  dvlog2lem  20015  ang180lem3  20125  atanlogaddlem  20225  atanlogsublem  20227  atantan  20235  atans2  20243  cxploglim2  20289  emcllem6  20310  emcllem7  20311  ftalem1  20326  ftalem2  20327  ppinncl  20428  chtrpcl  20429  vmalelog  20460  chtub  20467  logfacubnd  20476  logfacbnd3  20478  logfacrlim  20479  logexprlim  20480  mersenne  20482  perfectlem2  20485  bpos1lem  20537  bposlem1  20539  bposlem2  20540  bposlem3  20541  bposlem4  20542  bposlem5  20543  bposlem6  20544  lgseisen  20608  lgsquadlem1  20609  chebbnd1lem1  20634  chebbnd1lem3  20636  rpvmasumlem  20652  dchrvmasumlem2  20663  dchrvmasumlema  20665  dchrvmasumiflem1  20666  dchrisum0flblem2  20674  dchrisum0fno1  20676  dchrisum0re  20678  dirith2  20693  logdivsum  20698  mulog2sumlem1  20699  mulog2sumlem2  20700  log2sumbnd  20709  chpdifbndlem1  20718  chpdifbndlem2  20719  logdivbnd  20721  selberg3lem1  20722  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem3  20757  pntlemn  20765  pntlemj  20768  pntlemk  20771  pnt  20779  minvecolem4  21475  esumcvg2  23470  erdsze2lem2  23750  axlowdim  24661  pellqrex  27067  reglogltb  27079  reglogleb  27080  rmspecsqrnq  27094  rmspecnonsq  27095  rmspecpos  27104  lindfres  27396  fmul01  27813  stoweidlem26  27878  stoweidlem44  27896  stoweidlem45  27897  wallispilem3  27919  wallispi  27922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator