Theorem eqbrtrrid 5185

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  enpr1g  9020  undom  9059  undomOLD  9060  fidomdm  9329  prdom2  10001  infdju1  10184  infdif  10204  cfslb2n  10263  fin56  10388  dmct  10519  gchxpidm  10664  rankcf  10772  r1tskina  10777  tskuni  10778  ltsonq  10964  addgt0  11700  addgegt0  11701  addgtge0  11702  addge0  11703  expge1  14065  fsumrlim  15757  isumsup  15793  climcndslem1  15795  fprodge1  15939  3dvds  16274  bitsinv1lem  16382  phicl2  16701  frgpnabllem1  19741  lt6abl  19763  pgpfaclem2  19952  unitmulcl  20194  xrsdsreclblem  20991  znidomb  21117  lindfres  21378  gsumply1eq  21829  2ndcdisj2  22961  hmphindis  23301  tsms0  23646  tgptsmscls  23654  metustexhalf  24065  xrhmeo  24462  pcoass  24540  ovoliunlem1  25019  ismbl2  25044  voliunlem2  25068  ioombl1lem4  25078  itg2ge0  25253  itg2addlem  25276  itgge0  25328  dvfsumrlimge0  25547  abelthlem1  25943  abelthlem2  25944  pilem2  25964  cos0pilt1  26041  rplogcl  26112  logge0  26113  argimgt0  26120  logdivlti  26128  logf1o2  26158  dvlog2lem  26160  ang180lem3  26316  atanlogaddlem  26418  atanlogsublem  26420  atantan  26428  atans2  26436  cxploglim2  26483  emcllem6  26505  emcllem7  26506  lgamgulmlem2  26534  ftalem1  26577  ftalem2  26578  ppinncl  26678  chtrpcl  26679  vmalelog  26708  chtub  26715  logfacubnd  26724  logfacbnd3  26726  logfacrlim  26727  logexprlim  26728  mersenne  26730  perfectlem2  26733  bpos1lem  26785  bposlem1  26787  bposlem2  26788  bposlem3  26789  bposlem4  26790  bposlem5  26791  bposlem6  26792  lgseisen  26882  lgsquadlem1  26883  chebbnd1lem1  26972  chebbnd1lem3  26974  rpvmasumlem  26990  dchrvmasumlem2  27001  dchrvmasumlema  27003  dchrvmasumiflem1  27004  dchrisum0flblem2  27012  dchrisum0fno1  27014  dchrisum0re  27016  dirith2  27031  logdivsum  27036  mulog2sumlem1  27037  mulog2sumlem2  27038  log2sumbnd  27047  chpdifbndlem1  27056  chpdifbndlem2  27057  logdivbnd  27059  selberg3lem1  27060  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem3  27095  pntlemn  27103  pntlemj  27106  pntlemk  27109  pnt  27117  sltmulneg1d  27628  tgldimor  27753  axlowdim  28219  minvecolem4  30133  abrexct  31941  abrexctf  31943  nndiffz1  31997  wrdt2ind  32117  xrge0addgt0  32192  drngdimgt0  32703  esumcvg2  33085  inelcarsg  33310  carsgclctunlem2  33318  signsply0  33562  signsvtn  33595  erdsze2lem2  34195  lcmineqlem23  40916  lcmineqlem  40917  aks4d1p1p6  40938  aks4d1p1  40941  metakunt2  40986  metakunt29  41013  2xp3dxp2ge1d  41022  flt4lem7  41401  pellqrex  41617  reglogltb  41629  reglogleb  41630  rmspecnonsq  41645  rmspecpos  41655  areaquad  41965  hashnzfz2  43080  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  fmul01  44296  climconstmpt  44374  stoweidlem26  44742  stoweidlem44  44760  stoweidlem45  44761  wallispilem3  44783  wallispi  44786  stirlinglem11  44800  dirkertrigeqlem1  44814  dirkertrigeqlem3  44816  fourierdlem80  44902  fourierdlem102  44924  fourierdlem107  44929  fourierdlem114  44936  etransclem46  44996  fmtnoge3  46198  fmtno4prmfac  46240  perfectALTVlem2  46390  gboge9  46432  mogoldbb  46453  tgoldbach  46485  nnolog2flm1  47276