Theorem eqbrtrrid 5202

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 5199	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  enpr1g  9085  undom  9125  undomOLD  9126  fidomdm  9402  prdom2  10075  infdju1  10259  infdif  10277  cfslb2n  10337  fin56  10462  dmct  10593  gchxpidm  10738  rankcf  10846  r1tskina  10851  tskuni  10852  ltsonq  11038  addgt0  11776  addgegt0  11777  addgtge0  11778  addge0  11779  expge1  14150  fsumrlim  15859  isumsup  15895  climcndslem1  15897  fprodge1  16043  3dvds  16379  bitsinv1lem  16487  phicl2  16815  frgpnabllem1  19915  lt6abl  19937  pgpfaclem2  20126  unitmulcl  20406  xrsdsreclblem  21453  znidomb  21603  lindfres  21866  gsumply1eq  22334  2ndcdisj2  23486  hmphindis  23826  tsms0  24171  tgptsmscls  24179  metustexhalf  24590  xrhmeo  24996  pcoass  25076  ovoliunlem1  25556  ismbl2  25581  voliunlem2  25605  ioombl1lem4  25615  itg2ge0  25790  itg2addlem  25813  itgge0  25866  dvfsumrlimge0  26091  abelthlem1  26493  abelthlem2  26494  pilem2  26514  cos0pilt1  26592  rplogcl  26664  logge0  26665  argimgt0  26672  logdivlti  26680  logf1o2  26710  dvlog2lem  26712  ang180lem3  26872  atanlogaddlem  26974  atanlogsublem  26976  atantan  26984  atans2  26992  cxploglim2  27040  emcllem6  27062  emcllem7  27063  lgamgulmlem2  27091  ftalem1  27134  ftalem2  27135  ppinncl  27235  chtrpcl  27236  vmalelog  27267  chtub  27274  logfacubnd  27283  logfacbnd3  27285  logfacrlim  27286  logexprlim  27287  mersenne  27289  perfectlem2  27292  bpos1lem  27344  bposlem1  27346  bposlem2  27347  bposlem3  27348  bposlem4  27349  bposlem5  27350  bposlem6  27351  lgseisen  27441  lgsquadlem1  27442  chebbnd1lem1  27531  chebbnd1lem3  27533  rpvmasumlem  27549  dchrvmasumlem2  27560  dchrvmasumlema  27562  dchrvmasumiflem1  27563  dchrisum0flblem2  27571  dchrisum0fno1  27573  dchrisum0re  27575  dirith2  27590  logdivsum  27595  mulog2sumlem1  27596  mulog2sumlem2  27597  log2sumbnd  27606  chpdifbndlem1  27615  chpdifbndlem2  27616  logdivbnd  27618  selberg3lem1  27619  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem3  27654  pntlemn  27662  pntlemj  27665  pntlemk  27668  pnt  27676  addsgt0d  28065  sltmulneg1d  28220  absmuls  28286  abssge0  28287  sleabs  28290  nnsge1  28364  tgldimor  28528  axlowdim  28994  minvecolem4  30912  abrexct  32730  abrexctf  32732  nndiffz1  32791  wrdt2ind  32920  xrge0addgt0  33003  drngdimgt0  33631  esumcvg2  34051  inelcarsg  34276  carsgclctunlem2  34284  signsply0  34528  signsvtn  34561  erdsze2lem2  35172  lcmineqlem23  42008  lcmineqlem  42009  aks4d1p1p6  42030  aks4d1p1  42033  aks5lem2  42144  metakunt2  42163  metakunt29  42190  2xp3dxp2ge1d  42198  flt4lem7  42614  pellqrex  42835  reglogltb  42847  reglogleb  42848  rmspecnonsq  42863  rmspecpos  42873  areaquad  43177  hashnzfz2  44290  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  fmul01  45501  climconstmpt  45579  stoweidlem26  45947  stoweidlem44  45965  stoweidlem45  45966  wallispilem3  45988  wallispi  45991  stirlinglem11  46005  dirkertrigeqlem1  46019  dirkertrigeqlem3  46021  fourierdlem80  46107  fourierdlem102  46129  fourierdlem107  46134  fourierdlem114  46141  etransclem46  46201  fmtnoge3  47404  fmtno4prmfac  47446  perfectALTVlem2  47596  gboge9  47638  mogoldbb  47659  tgoldbach  47691  nnolog2flm1  48324