Theorem eqbrtrrid 5127

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092

This theorem is referenced by:  enpr1g  8945  undom  8978  fidomdm  9218  prdom2  9897  infdju1  10081  infdif  10099  cfslb2n  10159  fin56  10284  dmct  10415  gchxpidm  10560  rankcf  10668  r1tskina  10673  tskuni  10674  ltsonq  10860  addgt0  11603  addgegt0  11604  addgtge0  11605  addge0  11606  expge1  14006  fsumrlim  15718  isumsup  15754  climcndslem1  15756  fprodge1  15902  3dvds  16242  bitsinv1lem  16352  phicl2  16679  frgpnabllem1  19786  lt6abl  19808  pgpfaclem2  19997  unitmulcl  20299  xrsdsreclblem  21350  znidomb  21499  lindfres  21761  gsumply1eq  22225  2ndcdisj2  23373  hmphindis  23713  tsms0  24058  tgptsmscls  24066  metustexhalf  24472  xrhmeo  24872  pcoass  24952  ovoliunlem1  25431  ismbl2  25456  voliunlem2  25480  ioombl1lem4  25490  itg2ge0  25664  itg2addlem  25687  itgge0  25740  dvfsumrlimge0  25965  abelthlem1  26369  abelthlem2  26370  pilem2  26390  cos0pilt1  26469  rplogcl  26541  logge0  26542  argimgt0  26549  logdivlti  26557  logf1o2  26587  dvlog2lem  26589  ang180lem3  26749  atanlogaddlem  26851  atanlogsublem  26853  atantan  26861  atans2  26869  cxploglim2  26917  emcllem6  26939  emcllem7  26940  lgamgulmlem2  26968  ftalem1  27011  ftalem2  27012  ppinncl  27112  chtrpcl  27113  vmalelog  27144  chtub  27151  logfacubnd  27160  logfacbnd3  27162  logfacrlim  27163  logexprlim  27164  mersenne  27166  perfectlem2  27169  bpos1lem  27221  bposlem1  27223  bposlem2  27224  bposlem3  27225  bposlem4  27226  bposlem5  27227  bposlem6  27228  lgseisen  27318  lgsquadlem1  27319  chebbnd1lem1  27408  chebbnd1lem3  27410  rpvmasumlem  27426  dchrvmasumlem2  27437  dchrvmasumlema  27439  dchrvmasumiflem1  27440  dchrisum0flblem2  27448  dchrisum0fno1  27450  dchrisum0re  27452  dirith2  27467  logdivsum  27472  mulog2sumlem1  27473  mulog2sumlem2  27474  log2sumbnd  27483  chpdifbndlem1  27492  chpdifbndlem2  27493  logdivbnd  27495  selberg3lem1  27496  pntpbnd1a  27524  pntpbnd2  27526  pntibndlem3  27531  pntlemn  27539  pntlemj  27542  pntlemk  27545  pnt  27553  addsgt0d  27958  sltmulneg1d  28116  absmuls  28183  abssge0  28184  sleabs  28187  nnsge1  28272  tgldimor  28481  axlowdim  28940  minvecolem4  30858  abrexct  32696  abrexctf  32698  nndiffz1  32767  wrdt2ind  32932  xrge0addgt0  32996  elrgspnlem2  33208  drngdimgt0  33629  extdgfialglem2  33704  cos9thpiminplylem1  33793  esumcvg2  34098  inelcarsg  34322  carsgclctunlem2  34330  signsply0  34562  signsvtn  34595  erdsze2lem2  35246  lcmineqlem23  42090  lcmineqlem  42091  aks4d1p1p6  42112  aks4d1p1  42115  aks5lem2  42226  flt4lem7  42698  pellqrex  42918  reglogltb  42930  reglogleb  42931  rmspecnonsq  42946  rmspecpos  42955  areaquad  43255  hashnzfz2  44360  binomcxplemdvbinom  44392  binomcxplemnotnn0  44395  fmul01  45626  climconstmpt  45702  stoweidlem26  46070  stoweidlem44  46088  stoweidlem45  46089  wallispilem3  46111  wallispi  46114  stirlinglem11  46128  dirkertrigeqlem1  46142  dirkertrigeqlem3  46144  fourierdlem80  46230  fourierdlem102  46252  fourierdlem107  46257  fourierdlem114  46264  etransclem46  46324  fmtnoge3  47567  fmtno4prmfac  47609  perfectALTVlem2  47759  gboge9  47801  mogoldbb  47822  tgoldbach  47854  gpg3kgrtriexlem3  48122  gpg3kgrtriexlem6  48125  nnolog2flm1  48628