Theorem eqbrtrrid 5115

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

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080

This theorem is referenced by:  enpr1g  8967  undom  9000  fidomdm  9241  prdom2  9926  infdju1  10110  infdif  10128  cfslb2n  10188  fin56  10313  dmct  10444  gchxpidm  10590  rankcf  10698  r1tskina  10703  tskuni  10704  ltsonq  10890  addgt0  11634  addgegt0  11635  addgtge0  11636  addge0  11637  expge1  14059  fsumrlim  15772  isumsup  15810  climcndslem1  15812  fprodge1  15958  3dvds  16298  bitsinv1lem  16408  phicl2  16736  frgpnabllem1  19846  lt6abl  19868  pgpfaclem2  20057  unitmulcl  20358  xrsdsreclblem  21395  znidomb  21543  lindfres  21805  gsumply1eq  22302  2ndcdisj2  23447  hmphindis  23787  tsms0  24132  tgptsmscls  24140  metustexhalf  24546  xrhmeo  24938  pcoass  25016  ovoliunlem1  25494  ismbl2  25519  voliunlem2  25543  ioombl1lem4  25553  itg2ge0  25727  itg2addlem  25750  itgge0  25803  dvfsumrlimge0  26022  abelthlem1  26421  abelthlem2  26422  pilem2  26442  cos0pilt1  26521  rplogcl  26593  logge0  26594  argimgt0  26601  logdivlti  26609  logf1o2  26639  dvlog2lem  26641  ang180lem3  26800  atanlogaddlem  26902  atanlogsublem  26904  atantan  26912  atans2  26920  cxploglim2  26967  emcllem6  26989  emcllem7  26990  lgamgulmlem2  27018  ftalem1  27061  ftalem2  27062  ppinncl  27162  chtrpcl  27163  vmalelog  27193  chtub  27200  logfacubnd  27209  logfacbnd3  27211  logfacrlim  27212  logexprlim  27213  mersenne  27215  perfectlem2  27218  bpos1lem  27270  bposlem1  27272  bposlem2  27273  bposlem3  27274  bposlem4  27275  bposlem5  27276  bposlem6  27277  lgseisen  27367  lgsquadlem1  27368  chebbnd1lem1  27457  chebbnd1lem3  27459  rpvmasumlem  27475  dchrvmasumlem2  27486  dchrvmasumlema  27488  dchrvmasumiflem1  27489  dchrisum0flblem2  27497  dchrisum0fno1  27499  dchrisum0re  27501  dirith2  27516  logdivsum  27521  mulog2sumlem1  27522  mulog2sumlem2  27523  log2sumbnd  27532  chpdifbndlem1  27541  chpdifbndlem2  27542  logdivbnd  27544  selberg3lem1  27545  pntpbnd1a  27573  pntpbnd2  27575  pntibndlem3  27580  pntlemn  27588  pntlemj  27591  pntlemk  27594  pnt  27602  addsgt0d  28031  ltmulnegs1d  28193  absmuls  28261  abssge0  28262  leabss  28265  nnsge1  28360  bdayfinbndlem1  28484  tgldimor  28595  axlowdim  29055  minvecolem4  30976  abrexct  32814  abrexctf  32816  nndiffz1  32885  wrdt2ind  33039  xrge0addgt0  33103  elrgspnlem2  33331  ply1coedeg  33679  drngdimgt0  33809  extdgfialglem2  33884  cos9thpiminplylem1  33973  esumcvg2  34278  inelcarsg  34502  carsgclctunlem2  34510  signsply0  34742  signsvtn  34775  erdsze2lem2  35439  lcmineqlem23  42543  lcmineqlem  42544  aks4d1p1p6  42565  aks4d1p1  42568  aks5lem2  42679  flt4lem7  43116  pellqrex  43331  reglogltb  43343  reglogleb  43344  rmspecnonsq  43359  rmspecpos  43368  areaquad  43668  hashnzfz2  44772  binomcxplemdvbinom  44804  binomcxplemnotnn0  44807  fmul01  46032  climconstmpt  46108  stoweidlem26  46476  stoweidlem44  46494  stoweidlem45  46495  wallispilem3  46517  wallispi  46520  stirlinglem11  46534  dirkertrigeqlem1  46548  dirkertrigeqlem3  46550  fourierdlem80  46636  fourierdlem102  46658  fourierdlem107  46663  fourierdlem114  46670  etransclem46  46730  fmtnoge3  48015  fmtno4prmfac  48057  perfectALTVlem2  48220  gboge9  48262  mogoldbb  48283  tgoldbach  48315  gpg3kgrtriexlem3  48583  gpg3kgrtriexlem6  48586  nnolog2flm1  49088