Theorem eqbrtrrid 5183

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5147

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  enpr1g  9016  undom  9055  undomOLD  9056  fidomdm  9325  prdom2  9997  infdju1  10180  infdif  10200  cfslb2n  10259  fin56  10384  dmct  10515  gchxpidm  10660  rankcf  10768  r1tskina  10773  tskuni  10774  ltsonq  10960  addgt0  11696  addgegt0  11697  addgtge0  11698  addge0  11699  expge1  14061  fsumrlim  15753  isumsup  15789  climcndslem1  15791  fprodge1  15935  3dvds  16270  bitsinv1lem  16378  phicl2  16697  frgpnabllem1  19735  lt6abl  19757  pgpfaclem2  19946  unitmulcl  20186  xrsdsreclblem  20983  znidomb  21108  lindfres  21369  gsumply1eq  21820  2ndcdisj2  22952  hmphindis  23292  tsms0  23637  tgptsmscls  23645  metustexhalf  24056  xrhmeo  24453  pcoass  24531  ovoliunlem1  25010  ismbl2  25035  voliunlem2  25059  ioombl1lem4  25069  itg2ge0  25244  itg2addlem  25267  itgge0  25319  dvfsumrlimge0  25538  abelthlem1  25934  abelthlem2  25935  pilem2  25955  cos0pilt1  26032  rplogcl  26103  logge0  26104  argimgt0  26111  logdivlti  26119  logf1o2  26149  dvlog2lem  26151  ang180lem3  26305  atanlogaddlem  26407  atanlogsublem  26409  atantan  26417  atans2  26425  cxploglim2  26472  emcllem6  26494  emcllem7  26495  lgamgulmlem2  26523  ftalem1  26566  ftalem2  26567  ppinncl  26667  chtrpcl  26668  vmalelog  26697  chtub  26704  logfacubnd  26713  logfacbnd3  26715  logfacrlim  26716  logexprlim  26717  mersenne  26719  perfectlem2  26722  bpos1lem  26774  bposlem1  26776  bposlem2  26777  bposlem3  26778  bposlem4  26779  bposlem5  26780  bposlem6  26781  lgseisen  26871  lgsquadlem1  26872  chebbnd1lem1  26961  chebbnd1lem3  26963  rpvmasumlem  26979  dchrvmasumlem2  26990  dchrvmasumlema  26992  dchrvmasumiflem1  26993  dchrisum0flblem2  27001  dchrisum0fno1  27003  dchrisum0re  27005  dirith2  27020  logdivsum  27025  mulog2sumlem1  27026  mulog2sumlem2  27027  log2sumbnd  27036  chpdifbndlem1  27045  chpdifbndlem2  27046  logdivbnd  27048  selberg3lem1  27049  pntpbnd1a  27077  pntpbnd2  27079  pntibndlem3  27084  pntlemn  27092  pntlemj  27095  pntlemk  27098  pnt  27106  sltmulneg1d  27617  tgldimor  27742  axlowdim  28208  minvecolem4  30120  abrexct  31928  abrexctf  31930  nndiffz1  31984  wrdt2ind  32104  xrge0addgt0  32179  drngdimgt0  32691  esumcvg2  33073  inelcarsg  33298  carsgclctunlem2  33306  signsply0  33550  signsvtn  33583  erdsze2lem2  34183  lcmineqlem23  40904  lcmineqlem  40905  aks4d1p1p6  40926  aks4d1p1  40929  metakunt2  40974  metakunt29  41001  2xp3dxp2ge1d  41010  flt4lem7  41397  pellqrex  41602  reglogltb  41614  reglogleb  41615  rmspecnonsq  41630  rmspecpos  41640  areaquad  41950  hashnzfz2  43065  binomcxplemdvbinom  43097  binomcxplemnotnn0  43100  fmul01  44282  climconstmpt  44360  stoweidlem26  44728  stoweidlem44  44746  stoweidlem45  44747  wallispilem3  44769  wallispi  44772  stirlinglem11  44786  dirkertrigeqlem1  44800  dirkertrigeqlem3  44802  fourierdlem80  44888  fourierdlem102  44910  fourierdlem107  44915  fourierdlem114  44922  etransclem46  44982  fmtnoge3  46184  fmtno4prmfac  46226  perfectALTVlem2  46376  gboge9  46418  mogoldbb  46439  tgoldbach  46471  nnolog2flm1  47229