Theorem eqbrtrrid 5066

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

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5030

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  enpr1g  8558  undom  8588  fidomdm  8785  prdom2  9417  infdju1  9600  infdif  9620  cfslb2n  9679  fin56  9804  dmct  9935  gchxpidm  10080  rankcf  10188  r1tskina  10193  tskuni  10194  ltsonq  10380  addgt0  11115  addgegt0  11116  addgtge0  11117  addge0  11118  expge1  13462  fsumrlim  15158  isumsup  15194  climcndslem1  15196  fprodge1  15341  3dvds  15672  bitsinv1lem  15780  phicl2  16095  frgpnabllem1  18986  lt6abl  19008  pgpfaclem2  19197  unitmulcl  19410  xrsdsreclblem  20137  znidomb  20253  lindfres  20512  gsumply1eq  20934  2ndcdisj2  22062  hmphindis  22402  tsms0  22747  tgptsmscls  22755  metustexhalf  23163  xrhmeo  23551  pcoass  23629  ovoliunlem1  24106  ismbl2  24131  voliunlem2  24155  ioombl1lem4  24165  itg2ge0  24339  itg2addlem  24362  itgge0  24414  dvfsumrlimge0  24633  abelthlem1  25026  abelthlem2  25027  pilem2  25047  cos0pilt1  25124  rplogcl  25195  logge0  25196  argimgt0  25203  logdivlti  25211  logf1o2  25241  dvlog2lem  25243  ang180lem3  25397  atanlogaddlem  25499  atanlogsublem  25501  atantan  25509  atans2  25517  cxploglim2  25564  emcllem6  25586  emcllem7  25587  lgamgulmlem2  25615  ftalem1  25658  ftalem2  25659  ppinncl  25759  chtrpcl  25760  vmalelog  25789  chtub  25796  logfacubnd  25805  logfacbnd3  25807  logfacrlim  25808  logexprlim  25809  mersenne  25811  perfectlem2  25814  bpos1lem  25866  bposlem1  25868  bposlem2  25869  bposlem3  25870  bposlem4  25871  bposlem5  25872  bposlem6  25873  lgseisen  25963  lgsquadlem1  25964  chebbnd1lem1  26053  chebbnd1lem3  26055  rpvmasumlem  26071  dchrvmasumlem2  26082  dchrvmasumlema  26084  dchrvmasumiflem1  26085  dchrisum0flblem2  26093  dchrisum0fno1  26095  dchrisum0re  26097  dirith2  26112  logdivsum  26117  mulog2sumlem1  26118  mulog2sumlem2  26119  log2sumbnd  26128  chpdifbndlem1  26137  chpdifbndlem2  26138  logdivbnd  26140  selberg3lem1  26141  pntpbnd1a  26169  pntpbnd2  26171  pntibndlem3  26176  pntlemn  26184  pntlemj  26187  pntlemk  26190  pnt  26198  tgldimor  26296  axlowdim  26755  minvecolem4  28663  abrexct  30478  abrexctf  30480  nndiffz1  30535  wrdt2ind  30653  xrge0addgt0  30725  drngdimgt0  31104  esumcvg2  31456  inelcarsg  31679  carsgclctunlem2  31687  signsply0  31931  signsvtn  31964  erdsze2lem2  32564  lcmineqlem23  39339  lcmineqlem  39340  metakunt2  39351  metakunt29  39378  2xp3dxp2ge1d  39387  pellqrex  39820  reglogltb  39832  reglogleb  39833  rmspecnonsq  39848  rmspecpos  39857  areaquad  40166  hashnzfz2  41025  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  fmul01  42222  climconstmpt  42300  stoweidlem26  42668  stoweidlem44  42686  stoweidlem45  42687  wallispilem3  42709  wallispi  42712  stirlinglem11  42726  dirkertrigeqlem1  42740  dirkertrigeqlem3  42742  fourierdlem80  42828  fourierdlem102  42850  fourierdlem107  42855  fourierdlem114  42862  etransclem46  42922  fmtnoge3  44047  fmtno4prmfac  44089  perfectALTVlem2  44240  gboge9  44282  mogoldbb  44303  tgoldbach  44335  nnolog2flm1  45004