Theorem eqbrtrrid 5140

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  enpr1g  9054  undom  9088  fidomdm  9327  resfifsupp  9393  prdom2  10089  infdju1  10272  infdif  10290  cfslb2n  10350  fin56  10475  dmct  10606  dmctOLD  10607  gchxpidm  10758  rankcf  10866  r1tskina  10871  tskuni  10872  ltsonq  11058  addgt0  11806  addgegt0  11807  addgtge0  11808  addge0  11809  expge1  14246  fsumrlim  15984  isumsup  16022  climcndslem1  16024  fprodge1  16168  3dvds  16507  bitsinv1lem  16617  phicl2  16951  frgpnabllem1  20093  lt6abl  20115  pgpfaclem2  20304  unitmulcl  20616  xrsdsreclblem  21725  znidomb  21873  lindfres  22135  gsumply1eq  22633  abrexct  23779  2ndcdisj2  23782  hmphindis  24122  tsms0  24467  tgptsmscls  24475  metustexhalf  24881  xrhmeo  25273  pcoass  25351  ovoliunlem1  25829  ismbl2  25854  voliunlem2  25878  ioombl1lem4  25888  itg2ge0  26062  itg2addlem  26085  itgge0  26137  dvfsumrlimge0  26356  abelthlem1  26764  abelthlem2  26765  pilem2  26785  cos0pilt1  26866  rplogcl  26938  logge0  26939  argimgt0  26946  logdivlti  26954  logf1o2  26984  dvlog2lem  26986  ang180lem3  27145  atanlogaddlem  27247  atanlogsublem  27249  atantan  27257  atans2  27265  cxploglim2  27312  emcllem6  27334  emcllem7  27335  lgamgulmlem2  27363  ftalem1  27406  ftalem2  27407  ppinncl  27507  chtrpcl  27508  vmalelog  27538  chtub  27545  logfacubnd  27554  logfacbnd3  27556  logfacrlim  27557  logexprlim  27558  mersenne  27560  perfectlem2  27563  bpos1lem  27615  bposlem1  27617  bposlem2  27618  bposlem3  27619  bposlem4  27620  bposlem5  27621  bposlem6  27622  lgseisen  27712  lgsquadlem1  27713  chebbnd1lem1  27802  chebbnd1lem3  27804  rpvmasumlem  27820  dchrvmasumlem2  27831  dchrvmasumlema  27833  dchrvmasumiflem1  27834  dchrisum0flblem2  27842  dchrisum0fno1  27844  dchrisum0re  27846  dirith2  27861  logdivsum  27866  mulog2sumlem1  27867  mulog2sumlem2  27868  log2sumbnd  27877  chpdifbndlem1  27886  chpdifbndlem2  27887  logdivbnd  27889  selberg3lem1  27890  pntpbnd1a  27918  pntpbnd2  27920  pntibndlem3  27925  pntlemn  27933  pntlemj  27936  pntlemk  27939  pnt  27947  fltoprmlem2  28000  addsgt0d  28406  ltmulnegs1d  28568  absmuls  28636  abssge0  28637  leabss  28640  nnsge1  28735  bdayfinbndlem1  28859  tgldimor  28971  axlowdim  29545  minvecolem4  31488  abrexctf  33357  nndiffz1  33425  wrdt2ind  33563  xrge0addgt0  33625  elrgspnlem2  33851  ply1coedeg  34168  drngdimgt0  34297  extdgfialglem2  34372  cos9thpiminplylem1  34461  esumcvg2  34766  inelcarsg  34990  carsgclctunlem2  34998  signsply0  35227  signsvtn  35260  erdsze2lem2  36056  lcmineqlem23  43195  lcmineqlem  43196  aks4d1p1p6  43217  aks4d1p1  43220  aks5lem2  43331  pellqrex  43980  reglogltb  43992  reglogleb  43993  rmspecnonsq  44008  rmspecpos  44017  areaquad  44312  hashnzfz2  45399  binomcxplemdvbinom  45431  binomcxplemnotnn0  45434  fmul01  46686  climconstmpt  46762  stoweidlem26  47130  stoweidlem44  47148  stoweidlem45  47149  wallispilem3  47171  wallispi  47174  stirlinglem11  47188  dirkertrigeqlem1  47202  dirkertrigeqlem3  47204  fourierdlem80  47290  fourierdlem102  47312  fourierdlem107  47317  fourierdlem114  47324  etransclem46  47384  fmtnoge3  48709  fmtno4prmfac  48751  perfectALTVlem2  48914  gboge9  48956  mogoldbb  48977  tgoldbach  49009  gpg3kgrtriexlem3  49277  gpg3kgrtriexlem6  49280  nnolog2flm1  49796