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

Syntax hints:   → wi 4   = wceq 1536   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 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  enpr1g  9061  undom  9097  undomOLD  9098  fidomdm  9371  prdom2  10043  infdju1  10227  infdif  10245  cfslb2n  10305  fin56  10430  dmct  10561  gchxpidm  10706  rankcf  10814  r1tskina  10819  tskuni  10820  ltsonq  11006  addgt0  11746  addgegt0  11747  addgtge0  11748  addge0  11749  expge1  14136  fsumrlim  15843  isumsup  15879  climcndslem1  15881  fprodge1  16027  3dvds  16364  bitsinv1lem  16474  phicl2  16801  frgpnabllem1  19905  lt6abl  19927  pgpfaclem2  20116  unitmulcl  20396  xrsdsreclblem  21447  znidomb  21597  lindfres  21860  gsumply1eq  22328  2ndcdisj2  23480  hmphindis  23820  tsms0  24165  tgptsmscls  24173  metustexhalf  24584  xrhmeo  24990  pcoass  25070  ovoliunlem1  25550  ismbl2  25575  voliunlem2  25599  ioombl1lem4  25609  itg2ge0  25784  itg2addlem  25807  itgge0  25860  dvfsumrlimge0  26085  abelthlem1  26489  abelthlem2  26490  pilem2  26510  cos0pilt1  26588  rplogcl  26660  logge0  26661  argimgt0  26668  logdivlti  26676  logf1o2  26706  dvlog2lem  26708  ang180lem3  26868  atanlogaddlem  26970  atanlogsublem  26972  atantan  26980  atans2  26988  cxploglim2  27036  emcllem6  27058  emcllem7  27059  lgamgulmlem2  27087  ftalem1  27130  ftalem2  27131  ppinncl  27231  chtrpcl  27232  vmalelog  27263  chtub  27270  logfacubnd  27279  logfacbnd3  27281  logfacrlim  27282  logexprlim  27283  mersenne  27285  perfectlem2  27288  bpos1lem  27340  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  lgseisen  27437  lgsquadlem1  27438  chebbnd1lem1  27527  chebbnd1lem3  27529  rpvmasumlem  27545  dchrvmasumlem2  27556  dchrvmasumlema  27558  dchrvmasumiflem1  27559  dchrisum0flblem2  27567  dchrisum0fno1  27569  dchrisum0re  27571  dirith2  27586  logdivsum  27591  mulog2sumlem1  27592  mulog2sumlem2  27593  log2sumbnd  27602  chpdifbndlem1  27611  chpdifbndlem2  27612  logdivbnd  27614  selberg3lem1  27615  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem3  27650  pntlemn  27658  pntlemj  27661  pntlemk  27664  pnt  27672  addsgt0d  28061  sltmulneg1d  28216  absmuls  28282  abssge0  28283  sleabs  28286  nnsge1  28360  tgldimor  28524  axlowdim  28990  minvecolem4  30908  abrexct  32733  abrexctf  32735  nndiffz1  32794  wrdt2ind  32922  xrge0addgt0  33004  elrgspnlem2  33232  drngdimgt0  33645  esumcvg2  34067  inelcarsg  34292  carsgclctunlem2  34300  signsply0  34544  signsvtn  34577  erdsze2lem2  35188  lcmineqlem23  42032  lcmineqlem  42033  aks4d1p1p6  42054  aks4d1p1  42057  aks5lem2  42168  metakunt2  42187  metakunt29  42214  2xp3dxp2ge1d  42222  flt4lem7  42645  pellqrex  42866  reglogltb  42878  reglogleb  42879  rmspecnonsq  42894  rmspecpos  42904  areaquad  43204  hashnzfz2  44316  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  fmul01  45535  climconstmpt  45613  stoweidlem26  45981  stoweidlem44  45999  stoweidlem45  46000  wallispilem3  46022  wallispi  46025  stirlinglem11  46039  dirkertrigeqlem1  46053  dirkertrigeqlem3  46055  fourierdlem80  46141  fourierdlem102  46163  fourierdlem107  46168  fourierdlem114  46175  etransclem46  46235  fmtnoge3  47454  fmtno4prmfac  47496  perfectALTVlem2  47646  gboge9  47688  mogoldbb  47709  tgoldbach  47741  nnolog2flm1  48439