Theorem syl5eqbrr 4924

Description: A chained equality inference for a binary relation. (Contributed by NM, 17-Sep-2004.)

Hypotheses

Ref	Expression
syl5eqbrr.1	⊢ 𝐵 = 𝐴
syl5eqbrr.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
syl5eqbrr	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem syl5eqbrr

Step	Hyp	Ref	Expression
1		syl5eqbrr.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		syl5eqbrr.1	. 2 ⊢ 𝐵 = 𝐴
3		eqid 2778	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr3g 4921	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1601   class class class wbr 4888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4889

This theorem is referenced by:  enpr1g  8309  undom  8338  fidomdm  8533  prdom2  9164  infdif  9368  cfslb2n  9427  dmct  9683  gchxpidm  9828  rankcf  9936  r1tskina  9941  tskuni  9942  ltsonq  10128  addgt0  10864  addgegt0  10865  addgtge0  10866  addge0  10867  expge1  13220  fsumrlim  14956  isumsup  14992  climcndslem1  14994  fprodge1  15137  3dvds  15469  bitsinv1lem  15579  phicl2  15888  frgpnabllem1  18673  lt6abl  18693  pgpfaclem2  18879  unitmulcl  19062  gsumply1eq  20082  xrsdsreclblem  20199  znidomb  20316  lindfres  20577  2ndcdisj2  21680  hmphindis  22020  tsms0  22364  tgptsmscls  22372  metustexhalf  22780  xrhmeo  23164  pcoass  23242  ovoliunlem1  23717  ismbl2  23742  voliunlem2  23766  ioombl1lem4  23776  itg2ge0  23950  itg2addlem  23973  itgge0  24025  dvfsumrlimge0  24241  abelthlem1  24633  abelthlem2  24634  pilem2  24654  rplogcl  24798  logge0  24799  argimgt0  24806  logdivlti  24814  logf1o2  24844  dvlog2lem  24846  ang180lem3  25000  atanlogaddlem  25102  atanlogsublem  25104  atantan  25112  atans2  25120  cxploglim2  25168  emcllem6  25190  emcllem7  25191  lgamgulmlem2  25219  ftalem1  25262  ftalem2  25263  ppinncl  25363  chtrpcl  25364  vmalelog  25393  chtub  25400  logfacubnd  25409  logfacbnd3  25411  logfacrlim  25412  logexprlim  25413  mersenne  25415  perfectlem2  25418  bpos1lem  25470  bposlem1  25472  bposlem2  25473  bposlem3  25474  bposlem4  25475  bposlem5  25476  bposlem6  25477  lgseisen  25567  lgsquadlem1  25568  chebbnd1lem1  25627  chebbnd1lem3  25629  rpvmasumlem  25645  dchrvmasumlem2  25656  dchrvmasumlema  25658  dchrvmasumiflem1  25659  dchrisum0flblem2  25667  dchrisum0fno1  25669  dchrisum0re  25671  dirith2  25686  logdivsum  25691  mulog2sumlem1  25692  mulog2sumlem2  25693  log2sumbnd  25702  chpdifbndlem1  25711  chpdifbndlem2  25712  logdivbnd  25714  selberg3lem1  25715  pntpbnd1a  25743  pntpbnd2  25745  pntibndlem3  25750  pntlemn  25758  pntlemj  25761  pntlemk  25764  pnt  25772  tgldimor  25870  axlowdim  26327  minvecolem4  28325  abrexct  30077  abrexctf  30079  nndiffz1  30126  xrge0addgt0  30261  esumcvg2  30755  inelcarsg  30979  carsgclctunlem2  30987  signsply0  31236  signsvtn  31271  erdsze2lem2  31793  pellqrex  38417  reglogltb  38429  reglogleb  38430  rmspecnonsq  38445  rmspecpos  38454  areaquad  38774  hashnzfz2  39490  binomcxplemdvbinom  39522  binomcxplemnotnn0  39525  fmul01  40734  climconstmpt  40812  stoweidlem26  41184  stoweidlem44  41202  stoweidlem45  41203  wallispilem3  41225  wallispi  41228  stirlinglem11  41242  dirkertrigeqlem1  41256  dirkertrigeqlem3  41258  fourierdlem80  41344  fourierdlem102  41366  fourierdlem107  41371  fourierdlem114  41378  etransclem46  41438  fmtnoge3  42477  fmtno4prmfac  42519  perfectALTVlem2  42670  gboge9  42691  mogoldbb  42712  tgoldbach  42744  nnolog2flm1  43413