Theorem eqbrtrrid 5122

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

Hypotheses

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

Assertion

Ref	Expression
eqbrtrrid	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrrid

Step	Hyp	Ref	Expression
1		eqbrtrrid.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrrid.1	. 2 ⊢ 𝐵 = 𝐴
3		eqid 2737	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr3g 5119	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  enpr1g  8961  undom  8994  fidomdm  9235  prdom2  9917  infdju1  10101  infdif  10119  cfslb2n  10179  fin56  10304  dmct  10435  gchxpidm  10581  rankcf  10689  r1tskina  10694  tskuni  10695  ltsonq  10881  addgt0  11624  addgegt0  11625  addgtge0  11626  addge0  11627  expge1  14023  fsumrlim  15735  isumsup  15771  climcndslem1  15773  fprodge1  15919  3dvds  16259  bitsinv1lem  16369  phicl2  16696  frgpnabllem1  19806  lt6abl  19828  pgpfaclem2  20017  unitmulcl  20318  xrsdsreclblem  21369  znidomb  21518  lindfres  21780  gsumply1eq  22252  2ndcdisj2  23400  hmphindis  23740  tsms0  24085  tgptsmscls  24093  metustexhalf  24499  xrhmeo  24891  pcoass  24969  ovoliunlem1  25447  ismbl2  25472  voliunlem2  25496  ioombl1lem4  25506  itg2ge0  25680  itg2addlem  25703  itgge0  25756  dvfsumrlimge0  25978  abelthlem1  26381  abelthlem2  26382  pilem2  26402  cos0pilt1  26481  rplogcl  26553  logge0  26554  argimgt0  26561  logdivlti  26569  logf1o2  26599  dvlog2lem  26601  ang180lem3  26761  atanlogaddlem  26863  atanlogsublem  26865  atantan  26873  atans2  26881  cxploglim2  26929  emcllem6  26951  emcllem7  26952  lgamgulmlem2  26980  ftalem1  27023  ftalem2  27024  ppinncl  27124  chtrpcl  27125  vmalelog  27156  chtub  27163  logfacubnd  27172  logfacbnd3  27174  logfacrlim  27175  logexprlim  27176  mersenne  27178  perfectlem2  27181  bpos1lem  27233  bposlem1  27235  bposlem2  27236  bposlem3  27237  bposlem4  27238  bposlem5  27239  bposlem6  27240  lgseisen  27330  lgsquadlem1  27331  chebbnd1lem1  27420  chebbnd1lem3  27422  rpvmasumlem  27438  dchrvmasumlem2  27449  dchrvmasumlema  27451  dchrvmasumiflem1  27452  dchrisum0flblem2  27460  dchrisum0fno1  27462  dchrisum0re  27464  dirith2  27479  logdivsum  27484  mulog2sumlem1  27485  mulog2sumlem2  27486  log2sumbnd  27495  chpdifbndlem1  27504  chpdifbndlem2  27505  logdivbnd  27507  selberg3lem1  27508  pntpbnd1a  27536  pntpbnd2  27538  pntibndlem3  27543  pntlemn  27551  pntlemj  27554  pntlemk  27557  pnt  27565  addsgt0d  27994  ltmulnegs1d  28156  absmuls  28224  abssge0  28225  leabss  28228  nnsge1  28323  bdayfinbndlem1  28447  tgldimor  28558  axlowdim  29018  minvecolem4  30940  abrexct  32777  abrexctf  32779  nndiffz1  32849  wrdt2ind  33018  xrge0addgt0  33082  elrgspnlem2  33309  ply1coedeg  33654  drngdimgt0  33768  extdgfialglem2  33843  cos9thpiminplylem1  33932  esumcvg2  34237  inelcarsg  34461  carsgclctunlem2  34469  signsply0  34701  signsvtn  34734  erdsze2lem2  35392  lcmineqlem23  42482  lcmineqlem  42483  aks4d1p1p6  42504  aks4d1p1  42507  aks5lem2  42618  flt4lem7  43091  pellqrex  43310  reglogltb  43322  reglogleb  43323  rmspecnonsq  43338  rmspecpos  43347  areaquad  43647  hashnzfz2  44751  binomcxplemdvbinom  44783  binomcxplemnotnn0  44786  fmul01  46014  climconstmpt  46090  stoweidlem26  46458  stoweidlem44  46476  stoweidlem45  46477  wallispilem3  46499  wallispi  46502  stirlinglem11  46516  dirkertrigeqlem1  46530  dirkertrigeqlem3  46532  fourierdlem80  46618  fourierdlem102  46640  fourierdlem107  46645  fourierdlem114  46652  etransclem46  46712  fmtnoge3  47964  fmtno4prmfac  48006  perfectALTVlem2  48156  gboge9  48198  mogoldbb  48219  tgoldbach  48251  gpg3kgrtriexlem3  48519  gpg3kgrtriexlem6  48522  nnolog2flm1  49024