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

Syntax hints:   → wi 4   = wceq 1542   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 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3848  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031

This theorem is referenced by:  enpr1g  8622  undom  8654  fidomdm  8874  prdom2  9506  infdju1  9689  infdif  9709  cfslb2n  9768  fin56  9893  dmct  10024  gchxpidm  10169  rankcf  10277  r1tskina  10282  tskuni  10283  ltsonq  10469  addgt0  11204  addgegt0  11205  addgtge0  11206  addge0  11207  expge1  13558  fsumrlim  15259  isumsup  15295  climcndslem1  15297  fprodge1  15441  3dvds  15776  bitsinv1lem  15884  phicl2  16205  frgpnabllem1  19112  lt6abl  19134  pgpfaclem2  19323  unitmulcl  19536  xrsdsreclblem  20263  znidomb  20380  lindfres  20639  gsumply1eq  21080  2ndcdisj2  22208  hmphindis  22548  tsms0  22893  tgptsmscls  22901  metustexhalf  23309  xrhmeo  23698  pcoass  23776  ovoliunlem1  24254  ismbl2  24279  voliunlem2  24303  ioombl1lem4  24313  itg2ge0  24488  itg2addlem  24511  itgge0  24563  dvfsumrlimge0  24782  abelthlem1  25178  abelthlem2  25179  pilem2  25199  cos0pilt1  25276  rplogcl  25347  logge0  25348  argimgt0  25355  logdivlti  25363  logf1o2  25393  dvlog2lem  25395  ang180lem3  25549  atanlogaddlem  25651  atanlogsublem  25653  atantan  25661  atans2  25669  cxploglim2  25716  emcllem6  25738  emcllem7  25739  lgamgulmlem2  25767  ftalem1  25810  ftalem2  25811  ppinncl  25911  chtrpcl  25912  vmalelog  25941  chtub  25948  logfacubnd  25957  logfacbnd3  25959  logfacrlim  25960  logexprlim  25961  mersenne  25963  perfectlem2  25966  bpos1lem  26018  bposlem1  26020  bposlem2  26021  bposlem3  26022  bposlem4  26023  bposlem5  26024  bposlem6  26025  lgseisen  26115  lgsquadlem1  26116  chebbnd1lem1  26205  chebbnd1lem3  26207  rpvmasumlem  26223  dchrvmasumlem2  26234  dchrvmasumlema  26236  dchrvmasumiflem1  26237  dchrisum0flblem2  26245  dchrisum0fno1  26247  dchrisum0re  26249  dirith2  26264  logdivsum  26269  mulog2sumlem1  26270  mulog2sumlem2  26271  log2sumbnd  26280  chpdifbndlem1  26289  chpdifbndlem2  26290  logdivbnd  26292  selberg3lem1  26293  pntpbnd1a  26321  pntpbnd2  26323  pntibndlem3  26328  pntlemn  26336  pntlemj  26339  pntlemk  26342  pnt  26350  tgldimor  26448  axlowdim  26907  minvecolem4  28815  abrexct  30626  abrexctf  30628  nndiffz1  30682  wrdt2ind  30800  xrge0addgt0  30877  drngdimgt0  31273  esumcvg2  31625  inelcarsg  31848  carsgclctunlem2  31856  signsply0  32100  signsvtn  32133  erdsze2lem2  32737  lcmineqlem23  39679  lcmineqlem  39680  aks4d1p1p6  39700  aks4d1p1  39703  metakunt2  39717  metakunt29  39744  2xp3dxp2ge1d  39753  flt4lem7  40068  pellqrex  40273  reglogltb  40285  reglogleb  40286  rmspecnonsq  40301  rmspecpos  40310  areaquad  40619  hashnzfz2  41477  binomcxplemdvbinom  41509  binomcxplemnotnn0  41512  fmul01  42663  climconstmpt  42741  stoweidlem26  43109  stoweidlem44  43127  stoweidlem45  43128  wallispilem3  43150  wallispi  43153  stirlinglem11  43167  dirkertrigeqlem1  43181  dirkertrigeqlem3  43183  fourierdlem80  43269  fourierdlem102  43291  fourierdlem107  43296  fourierdlem114  43303  etransclem46  43363  fmtnoge3  44516  fmtno4prmfac  44558  perfectALTVlem2  44708  gboge9  44750  mogoldbb  44771  tgoldbach  44803  nnolog2flm1  45470