Theorem eqbrtrrid 5110

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5074

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  enpr1g  8810  undom  8846  undomOLD  8847  fidomdm  9096  prdom2  9762  infdju1  9945  infdif  9965  cfslb2n  10024  fin56  10149  dmct  10280  gchxpidm  10425  rankcf  10533  r1tskina  10538  tskuni  10539  ltsonq  10725  addgt0  11461  addgegt0  11462  addgtge0  11463  addge0  11464  expge1  13820  fsumrlim  15523  isumsup  15559  climcndslem1  15561  fprodge1  15705  3dvds  16040  bitsinv1lem  16148  phicl2  16469  frgpnabllem1  19474  lt6abl  19496  pgpfaclem2  19685  unitmulcl  19906  xrsdsreclblem  20644  znidomb  20769  lindfres  21030  gsumply1eq  21476  2ndcdisj2  22608  hmphindis  22948  tsms0  23293  tgptsmscls  23301  metustexhalf  23712  xrhmeo  24109  pcoass  24187  ovoliunlem1  24666  ismbl2  24691  voliunlem2  24715  ioombl1lem4  24725  itg2ge0  24900  itg2addlem  24923  itgge0  24975  dvfsumrlimge0  25194  abelthlem1  25590  abelthlem2  25591  pilem2  25611  cos0pilt1  25688  rplogcl  25759  logge0  25760  argimgt0  25767  logdivlti  25775  logf1o2  25805  dvlog2lem  25807  ang180lem3  25961  atanlogaddlem  26063  atanlogsublem  26065  atantan  26073  atans2  26081  cxploglim2  26128  emcllem6  26150  emcllem7  26151  lgamgulmlem2  26179  ftalem1  26222  ftalem2  26223  ppinncl  26323  chtrpcl  26324  vmalelog  26353  chtub  26360  logfacubnd  26369  logfacbnd3  26371  logfacrlim  26372  logexprlim  26373  mersenne  26375  perfectlem2  26378  bpos1lem  26430  bposlem1  26432  bposlem2  26433  bposlem3  26434  bposlem4  26435  bposlem5  26436  bposlem6  26437  lgseisen  26527  lgsquadlem1  26528  chebbnd1lem1  26617  chebbnd1lem3  26619  rpvmasumlem  26635  dchrvmasumlem2  26646  dchrvmasumlema  26648  dchrvmasumiflem1  26649  dchrisum0flblem2  26657  dchrisum0fno1  26659  dchrisum0re  26661  dirith2  26676  logdivsum  26681  mulog2sumlem1  26682  mulog2sumlem2  26683  log2sumbnd  26692  chpdifbndlem1  26701  chpdifbndlem2  26702  logdivbnd  26704  selberg3lem1  26705  pntpbnd1a  26733  pntpbnd2  26735  pntibndlem3  26740  pntlemn  26748  pntlemj  26751  pntlemk  26754  pnt  26762  tgldimor  26863  axlowdim  27329  minvecolem4  29242  abrexct  31051  abrexctf  31053  nndiffz1  31107  wrdt2ind  31225  xrge0addgt0  31300  drngdimgt0  31701  esumcvg2  32055  inelcarsg  32278  carsgclctunlem2  32286  signsply0  32530  signsvtn  32563  erdsze2lem2  33166  lcmineqlem23  40059  lcmineqlem  40060  aks4d1p1p6  40081  aks4d1p1  40084  metakunt2  40126  metakunt29  40153  2xp3dxp2ge1d  40162  flt4lem7  40496  pellqrex  40701  reglogltb  40713  reglogleb  40714  rmspecnonsq  40729  rmspecpos  40738  areaquad  41047  hashnzfz2  41939  binomcxplemdvbinom  41971  binomcxplemnotnn0  41974  fmul01  43121  climconstmpt  43199  stoweidlem26  43567  stoweidlem44  43585  stoweidlem45  43586  wallispilem3  43608  wallispi  43611  stirlinglem11  43625  dirkertrigeqlem1  43639  dirkertrigeqlem3  43641  fourierdlem80  43727  fourierdlem102  43749  fourierdlem107  43754  fourierdlem114  43761  etransclem46  43821  fmtnoge3  44982  fmtno4prmfac  45024  perfectALTVlem2  45174  gboge9  45216  mogoldbb  45237  tgoldbach  45269  nnolog2flm1  45936