Theorem eqbrtrrid 5140

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

Syntax hints:   → wi 4   = wceq 1563   class class class wbr 5104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105

This theorem is referenced by:  enpr1g  9008  undom  9041  fidomdm  9279  resfifsupp  9345  prdom2  9978  infdju1  10161  infdif  10179  cfslb2n  10240  fin56  10365  dmct  10496  gchxpidm  10642  rankcf  10750  r1tskina  10755  tskuni  10756  ltsonq  10942  addgt0  11688  addgegt0  11689  addgtge0  11690  addge0  11691  expge1  14123  fsumrlim  15851  isumsup  15889  climcndslem1  15891  fprodge1  16037  3dvds  16377  bitsinv1lem  16487  phicl2  16815  frgpnabllem1  19931  lt6abl  19953  pgpfaclem2  20142  unitmulcl  20450  xrsdsreclblem  21520  znidomb  21668  lindfres  21930  gsumply1eq  22426  2ndcdisj2  23571  hmphindis  23911  tsms0  24256  tgptsmscls  24264  metustexhalf  24670  xrhmeo  25062  pcoass  25140  ovoliunlem1  25618  ismbl2  25643  voliunlem2  25667  ioombl1lem4  25677  itg2ge0  25851  itg2addlem  25874  itgge0  25927  dvfsumrlimge0  26146  abelthlem1  26548  abelthlem2  26549  pilem2  26569  cos0pilt1  26651  rplogcl  26723  logge0  26724  argimgt0  26731  logdivlti  26739  logf1o2  26769  dvlog2lem  26771  ang180lem3  26930  atanlogaddlem  27032  atanlogsublem  27034  atantan  27042  atans2  27050  cxploglim2  27097  emcllem6  27119  emcllem7  27120  lgamgulmlem2  27148  ftalem1  27191  ftalem2  27192  ppinncl  27292  chtrpcl  27293  vmalelog  27323  chtub  27330  logfacubnd  27339  logfacbnd3  27341  logfacrlim  27342  logexprlim  27343  mersenne  27345  perfectlem2  27348  bpos1lem  27400  bposlem1  27402  bposlem2  27403  bposlem3  27404  bposlem4  27405  bposlem5  27406  bposlem6  27407  lgseisen  27497  lgsquadlem1  27498  chebbnd1lem1  27587  chebbnd1lem3  27589  rpvmasumlem  27605  dchrvmasumlem2  27616  dchrvmasumlema  27618  dchrvmasumiflem1  27619  dchrisum0flblem2  27627  dchrisum0fno1  27629  dchrisum0re  27631  dirith2  27646  logdivsum  27651  mulog2sumlem1  27652  mulog2sumlem2  27653  log2sumbnd  27662  chpdifbndlem1  27671  chpdifbndlem2  27672  logdivbnd  27674  selberg3lem1  27675  pntpbnd1a  27703  pntpbnd2  27705  pntibndlem3  27710  pntlemn  27718  pntlemj  27721  pntlemk  27724  pnt  27732  addsgt0d  28161  ltmulnegs1d  28323  absmuls  28391  abssge0  28392  leabss  28395  nnsge1  28490  bdayfinbndlem1  28614  tgldimor  28725  axlowdim  29216  minvecolem4  31137  abrexct  32968  abrexctf  32970  nndiffz1  33039  wrdt2ind  33181  xrge0addgt0  33245  elrgspnlem2  33471  ply1coedeg  33791  drngdimgt0  33920  extdgfialglem2  33995  cos9thpiminplylem1  34084  esumcvg2  34389  inelcarsg  34613  carsgclctunlem2  34621  signsply0  34850  signsvtn  34883  erdsze2lem2  35562  lcmineqlem23  42675  lcmineqlem  42676  aks4d1p1p6  42697  aks4d1p1  42700  aks5lem2  42811  flt4lem7  43248  pellqrex  43463  reglogltb  43475  reglogleb  43476  rmspecnonsq  43491  rmspecpos  43500  areaquad  43800  hashnzfz2  44890  binomcxplemdvbinom  44922  binomcxplemnotnn0  44925  fmul01  46155  climconstmpt  46231  stoweidlem26  46599  stoweidlem44  46617  stoweidlem45  46618  wallispilem3  46640  wallispi  46643  stirlinglem11  46657  dirkertrigeqlem1  46671  dirkertrigeqlem3  46673  fourierdlem80  46759  fourierdlem102  46781  fourierdlem107  46786  fourierdlem114  46793  etransclem46  46853  fmtnoge3  48138  fmtno4prmfac  48180  perfectALTVlem2  48343  gboge9  48385  mogoldbb  48406  tgoldbach  48438  gpg3kgrtriexlem3  48706  gpg3kgrtriexlem6  48709  nnolog2flm1  49222