Theorem eqbrtrrid 5121

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 2736	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr3g 5118	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  enpr1g  8970  undom  9003  fidomdm  9244  prdom2  9928  infdju1  10112  infdif  10130  cfslb2n  10190  fin56  10315  dmct  10446  gchxpidm  10592  rankcf  10700  r1tskina  10705  tskuni  10706  ltsonq  10892  addgt0  11636  addgegt0  11637  addgtge0  11638  addge0  11639  expge1  14061  fsumrlim  15774  isumsup  15812  climcndslem1  15814  fprodge1  15960  3dvds  16300  bitsinv1lem  16410  phicl2  16738  frgpnabllem1  19848  lt6abl  19870  pgpfaclem2  20059  unitmulcl  20360  xrsdsreclblem  21393  znidomb  21541  lindfres  21803  gsumply1eq  22274  2ndcdisj2  23422  hmphindis  23762  tsms0  24107  tgptsmscls  24115  metustexhalf  24521  xrhmeo  24913  pcoass  24991  ovoliunlem1  25469  ismbl2  25494  voliunlem2  25518  ioombl1lem4  25528  itg2ge0  25702  itg2addlem  25725  itgge0  25778  dvfsumrlimge0  25997  abelthlem1  26396  abelthlem2  26397  pilem2  26417  cos0pilt1  26496  rplogcl  26568  logge0  26569  argimgt0  26576  logdivlti  26584  logf1o2  26614  dvlog2lem  26616  ang180lem3  26775  atanlogaddlem  26877  atanlogsublem  26879  atantan  26887  atans2  26895  cxploglim2  26942  emcllem6  26964  emcllem7  26965  lgamgulmlem2  26993  ftalem1  27036  ftalem2  27037  ppinncl  27137  chtrpcl  27138  vmalelog  27168  chtub  27175  logfacubnd  27184  logfacbnd3  27186  logfacrlim  27187  logexprlim  27188  mersenne  27190  perfectlem2  27193  bpos1lem  27245  bposlem1  27247  bposlem2  27248  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  lgseisen  27342  lgsquadlem1  27343  chebbnd1lem1  27432  chebbnd1lem3  27434  rpvmasumlem  27450  dchrvmasumlem2  27461  dchrvmasumlema  27463  dchrvmasumiflem1  27464  dchrisum0flblem2  27472  dchrisum0fno1  27474  dchrisum0re  27476  dirith2  27491  logdivsum  27496  mulog2sumlem1  27497  mulog2sumlem2  27498  log2sumbnd  27507  chpdifbndlem1  27516  chpdifbndlem2  27517  logdivbnd  27519  selberg3lem1  27520  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem3  27555  pntlemn  27563  pntlemj  27566  pntlemk  27569  pnt  27577  addsgt0d  28006  ltmulnegs1d  28168  absmuls  28236  abssge0  28237  leabss  28240  nnsge1  28335  bdayfinbndlem1  28459  tgldimor  28570  axlowdim  29030  minvecolem4  30951  abrexct  32788  abrexctf  32790  nndiffz1  32859  wrdt2ind  33013  xrge0addgt0  33077  elrgspnlem2  33304  ply1coedeg  33649  drngdimgt0  33762  extdgfialglem2  33837  cos9thpiminplylem1  33926  esumcvg2  34231  inelcarsg  34455  carsgclctunlem2  34463  signsply0  34695  signsvtn  34728  erdsze2lem2  35386  lcmineqlem23  42490  lcmineqlem  42491  aks4d1p1p6  42512  aks4d1p1  42515  aks5lem2  42626  flt4lem7  43092  pellqrex  43307  reglogltb  43319  reglogleb  43320  rmspecnonsq  43335  rmspecpos  43344  areaquad  43644  hashnzfz2  44748  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  fmul01  46010  climconstmpt  46086  stoweidlem26  46454  stoweidlem44  46472  stoweidlem45  46473  wallispilem3  46495  wallispi  46498  stirlinglem11  46512  dirkertrigeqlem1  46526  dirkertrigeqlem3  46528  fourierdlem80  46614  fourierdlem102  46636  fourierdlem107  46641  fourierdlem114  46648  etransclem46  46708  fmtnoge3  47993  fmtno4prmfac  48035  perfectALTVlem2  48198  gboge9  48240  mogoldbb  48261  tgoldbach  48293  gpg3kgrtriexlem3  48561  gpg3kgrtriexlem6  48564  nnolog2flm1  49066