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

Theorem syl5eqbrr 4460
Description: A 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 2429 . 2  |-  C  =  C
41, 2, 33brtr3g 4457 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427
This theorem is referenced by:  enpr1g  7642  undom  7666  fidomdm  7859  prdom2  8436  infdif  8637  cfslb2n  8696  gchxpidm  9093  rankcf  9201  r1tskina  9206  tskuni  9207  ltsonq  9393  addgt0  10099  addgegt0  10100  addgtge0  10101  addge0  10102  expge1  12306  fsumrlim  13849  isumsup  13883  climcndslem1  13885  3dvds  14347  bitsinv1lem  14389  phicl2  14685  frgpnabllem1  17444  lt6abl  17464  pgpfaclem2  17650  unitmulcl  17827  gsumply1eq  18834  xrsdsreclblem  18949  znidomb  19063  lindfres  19312  2ndcdisj2  20403  hmphindis  20743  tsms0  21087  tgptsmscls  21095  metustexhalf  21502  xrhmeo  21870  pcoass  21948  ovoliunlem1  22333  ismbl2  22358  voliunlem2  22381  ioombl1lem4  22391  itg2ge0  22570  itg2addlem  22593  itgge0  22645  dvfsumrlimge0  22859  abelthlem1  23251  abelthlem2  23252  pilem2  23272  pilem2OLD  23273  rplogcl  23418  logge0  23419  argimgt0  23426  logdivlti  23434  logf1o2  23460  dvlog2lem  23462  ang180lem3  23605  atanlogaddlem  23704  atanlogsublem  23706  atantan  23714  atans2  23722  cxploglim2  23769  emcllem6  23791  emcllem7  23792  lgamgulmlem2  23820  ftalem1  23862  ftalem2  23863  ppinncl  23964  chtrpcl  23965  vmalelog  23996  chtub  24003  logfacubnd  24012  logfacbnd3  24014  logfacrlim  24015  logexprlim  24016  mersenne  24018  perfectlem2  24021  bpos1lem  24073  bposlem1  24075  bposlem2  24076  bposlem3  24077  bposlem4  24078  bposlem5  24079  bposlem6  24080  lgseisen  24144  lgsquadlem1  24145  chebbnd1lem1  24170  chebbnd1lem3  24172  rpvmasumlem  24188  dchrvmasumlem2  24199  dchrvmasumlema  24201  dchrvmasumiflem1  24202  dchrisum0flblem2  24210  dchrisum0fno1  24212  dchrisum0re  24214  dirith2  24229  logdivsum  24234  mulog2sumlem1  24235  mulog2sumlem2  24236  log2sumbnd  24245  chpdifbndlem1  24254  chpdifbndlem2  24255  logdivbnd  24257  selberg3lem1  24258  pntpbnd1a  24286  pntpbnd2  24288  pntibndlem3  24293  pntlemn  24301  pntlemj  24304  pntlemk  24307  pnt  24315  tgldimor  24409  axlowdim  24837  minvecolem4  26367  dmct  28141  abrexct  28147  abrexctf  28149  nn0sqeq1  28167  nndiffz1  28202  xrge0addgt0  28292  esumcvg2  28747  inelcarsg  28972  carsgclctunlem2  28980  signsply0  29228  signsvtn  29261  erdsze2lem2  29715  pellqrex  35433  reglogltb  35445  reglogleb  35446  rmspecsqrtnq  35460  rmspecnonsq  35461  rmspecpos  35470  areaquad  35800  hashnzfz2  36307  binomcxplemdvbinom  36339  binomcxplemnotnn0  36342  fmul01  37230  stoweidlem26  37455  stoweidlem44  37474  stoweidlem45  37475  wallispilem3  37498  wallispi  37501  stirlinglem11  37515  dirkertrigeqlem1  37529  dirkertrigeqlem3  37531  fourierdlem80  37618  fourierdlem102  37640  fourierdlem107  37645  fourierdlem114  37652  etransclem46  37712  perfectALTVlem2  38234  gboage9  38255  tgoldbach  38301  nnolog2flm1  39162
  Copyright terms: Public domain W3C validator