Theorem eqbrtrrid 5131

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096

This theorem is referenced by:  enpr1g  8955  undom  8989  fidomdm  9243  prdom2  9919  infdju1  10103  infdif  10121  cfslb2n  10181  fin56  10306  dmct  10437  gchxpidm  10582  rankcf  10690  r1tskina  10695  tskuni  10696  ltsonq  10882  addgt0  11624  addgegt0  11625  addgtge0  11626  addge0  11627  expge1  14024  fsumrlim  15736  isumsup  15772  climcndslem1  15774  fprodge1  15920  3dvds  16260  bitsinv1lem  16370  phicl2  16697  frgpnabllem1  19770  lt6abl  19792  pgpfaclem2  19981  unitmulcl  20283  xrsdsreclblem  21337  znidomb  21486  lindfres  21748  gsumply1eq  22212  2ndcdisj2  23360  hmphindis  23700  tsms0  24045  tgptsmscls  24053  metustexhalf  24460  xrhmeo  24860  pcoass  24940  ovoliunlem1  25419  ismbl2  25444  voliunlem2  25468  ioombl1lem4  25478  itg2ge0  25652  itg2addlem  25675  itgge0  25728  dvfsumrlimge0  25953  abelthlem1  26357  abelthlem2  26358  pilem2  26378  cos0pilt1  26457  rplogcl  26529  logge0  26530  argimgt0  26537  logdivlti  26545  logf1o2  26575  dvlog2lem  26577  ang180lem3  26737  atanlogaddlem  26839  atanlogsublem  26841  atantan  26849  atans2  26857  cxploglim2  26905  emcllem6  26927  emcllem7  26928  lgamgulmlem2  26956  ftalem1  26999  ftalem2  27000  ppinncl  27100  chtrpcl  27101  vmalelog  27132  chtub  27139  logfacubnd  27148  logfacbnd3  27150  logfacrlim  27151  logexprlim  27152  mersenne  27154  perfectlem2  27157  bpos1lem  27209  bposlem1  27211  bposlem2  27212  bposlem3  27213  bposlem4  27214  bposlem5  27215  bposlem6  27216  lgseisen  27306  lgsquadlem1  27307  chebbnd1lem1  27396  chebbnd1lem3  27398  rpvmasumlem  27414  dchrvmasumlem2  27425  dchrvmasumlema  27427  dchrvmasumiflem1  27428  dchrisum0flblem2  27436  dchrisum0fno1  27438  dchrisum0re  27440  dirith2  27455  logdivsum  27460  mulog2sumlem1  27461  mulog2sumlem2  27462  log2sumbnd  27471  chpdifbndlem1  27480  chpdifbndlem2  27481  logdivbnd  27483  selberg3lem1  27484  pntpbnd1a  27512  pntpbnd2  27514  pntibndlem3  27519  pntlemn  27527  pntlemj  27530  pntlemk  27533  pnt  27541  addsgt0d  27944  sltmulneg1d  28102  absmuls  28169  abssge0  28170  sleabs  28173  nnsge1  28258  tgldimor  28465  axlowdim  28924  minvecolem4  30842  abrexct  32673  abrexctf  32675  nndiffz1  32742  wrdt2ind  32908  xrge0addgt0  32984  elrgspnlem2  33196  drngdimgt0  33593  cos9thpiminplylem1  33751  esumcvg2  34056  inelcarsg  34281  carsgclctunlem2  34289  signsply0  34521  signsvtn  34554  erdsze2lem2  35179  lcmineqlem23  42027  lcmineqlem  42028  aks4d1p1p6  42049  aks4d1p1  42052  aks5lem2  42163  flt4lem7  42635  pellqrex  42855  reglogltb  42867  reglogleb  42868  rmspecnonsq  42883  rmspecpos  42892  areaquad  43192  hashnzfz2  44297  binomcxplemdvbinom  44329  binomcxplemnotnn0  44332  fmul01  45565  climconstmpt  45643  stoweidlem26  46011  stoweidlem44  46029  stoweidlem45  46030  wallispilem3  46052  wallispi  46055  stirlinglem11  46069  dirkertrigeqlem1  46083  dirkertrigeqlem3  46085  fourierdlem80  46171  fourierdlem102  46193  fourierdlem107  46198  fourierdlem114  46205  etransclem46  46265  fmtnoge3  47518  fmtno4prmfac  47560  perfectALTVlem2  47710  gboge9  47752  mogoldbb  47773  tgoldbach  47805  gpg3kgrtriexlem3  48073  gpg3kgrtriexlem6  48076  nnolog2flm1  48579