Theorem eqbrtrrid 5148

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

Syntax hints:   → wi 4   = wceq 1570   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111

This theorem is referenced by:  enpr1g  9021  undom  9054  fidomdm  9292  resfifsupp  9358  prdom2  9991  infdju1  10174  infdif  10192  cfslb2n  10253  fin56  10378  dmct  10509  gchxpidm  10655  rankcf  10763  r1tskina  10768  tskuni  10769  ltsonq  10955  addgt0  11701  addgegt0  11702  addgtge0  11703  addge0  11704  expge1  14137  fsumrlim  15865  isumsup  15903  climcndslem1  15905  fprodge1  16051  3dvds  16390  bitsinv1lem  16500  phicl2  16828  frgpnabllem1  19944  lt6abl  19966  pgpfaclem2  20155  unitmulcl  20463  xrsdsreclblem  21544  znidomb  21692  lindfres  21954  gsumply1eq  22450  2ndcdisj2  23595  hmphindis  23935  tsms0  24280  tgptsmscls  24288  metustexhalf  24694  xrhmeo  25086  pcoass  25164  ovoliunlem1  25642  ismbl2  25667  voliunlem2  25691  ioombl1lem4  25701  itg2ge0  25875  itg2addlem  25898  itgge0  25951  dvfsumrlimge0  26170  abelthlem1  26575  abelthlem2  26576  pilem2  26596  cos0pilt1  26678  rplogcl  26750  logge0  26751  argimgt0  26758  logdivlti  26766  logf1o2  26796  dvlog2lem  26798  ang180lem3  26957  atanlogaddlem  27059  atanlogsublem  27061  atantan  27069  atans2  27077  cxploglim2  27124  emcllem6  27146  emcllem7  27147  lgamgulmlem2  27175  ftalem1  27218  ftalem2  27219  ppinncl  27319  chtrpcl  27320  vmalelog  27350  chtub  27357  logfacubnd  27366  logfacbnd3  27368  logfacrlim  27369  logexprlim  27370  mersenne  27372  perfectlem2  27375  bpos1lem  27427  bposlem1  27429  bposlem2  27430  bposlem3  27431  bposlem4  27432  bposlem5  27433  bposlem6  27434  lgseisen  27524  lgsquadlem1  27525  chebbnd1lem1  27614  chebbnd1lem3  27616  rpvmasumlem  27632  dchrvmasumlem2  27643  dchrvmasumlema  27645  dchrvmasumiflem1  27646  dchrisum0flblem2  27654  dchrisum0fno1  27656  dchrisum0re  27658  dirith2  27673  logdivsum  27678  mulog2sumlem1  27679  mulog2sumlem2  27680  log2sumbnd  27689  chpdifbndlem1  27698  chpdifbndlem2  27699  logdivbnd  27701  selberg3lem1  27702  pntpbnd1a  27730  pntpbnd2  27732  pntibndlem3  27737  pntlemn  27745  pntlemj  27748  pntlemk  27751  pnt  27759  addsgt0d  28188  ltmulnegs1d  28350  absmuls  28418  abssge0  28419  leabss  28422  nnsge1  28517  bdayfinbndlem1  28641  tgldimor  28752  axlowdim  29292  minvecolem4  31213  abrexct  33041  abrexctf  33043  nndiffz1  33112  wrdt2ind  33254  xrge0addgt0  33318  elrgspnlem2  33544  ply1coedeg  33860  drngdimgt0  33989  extdgfialglem2  34064  cos9thpiminplylem1  34153  esumcvg2  34458  inelcarsg  34682  carsgclctunlem2  34690  signsply0  34919  signsvtn  34952  erdsze2lem2  35677  lcmineqlem23  42799  lcmineqlem  42800  aks4d1p1p6  42821  aks4d1p1  42824  aks5lem2  42935  flt4lem7  43374  pellqrex  43589  reglogltb  43601  reglogleb  43602  rmspecnonsq  43617  rmspecpos  43626  areaquad  43926  hashnzfz2  45014  binomcxplemdvbinom  45046  binomcxplemnotnn0  45049  fmul01  46279  climconstmpt  46355  stoweidlem26  46723  stoweidlem44  46741  stoweidlem45  46742  wallispilem3  46764  wallispi  46767  stirlinglem11  46781  dirkertrigeqlem1  46795  dirkertrigeqlem3  46797  fourierdlem80  46883  fourierdlem102  46905  fourierdlem107  46910  fourierdlem114  46917  etransclem46  46977  fmtnoge3  48265  fmtno4prmfac  48307  perfectALTVlem2  48470  gboge9  48512  mogoldbb  48533  tgoldbach  48565  gpg3kgrtriexlem3  48833  gpg3kgrtriexlem6  48836  nnolog2flm1  49353