Theorem eqbrtrrid 5141

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  enpr1g  9034  undom  9068  fidomdm  9307  resfifsupp  9373  prdom2  10066  infdju1  10249  infdif  10267  cfslb2n  10327  fin56  10452  dmct  10583  dmctOLD  10584  gchxpidm  10735  rankcf  10843  r1tskina  10848  tskuni  10849  ltsonq  11035  addgt0  11783  addgegt0  11784  addgtge0  11785  addge0  11786  expge1  14222  fsumrlim  15958  isumsup  15996  climcndslem1  15998  fprodge1  16142  3dvds  16481  bitsinv1lem  16591  phicl2  16925  frgpnabllem1  20067  lt6abl  20089  pgpfaclem2  20278  unitmulcl  20590  xrsdsreclblem  21699  znidomb  21847  lindfres  22109  gsumply1eq  22607  abrexct  23753  2ndcdisj2  23756  hmphindis  24096  tsms0  24441  tgptsmscls  24449  metustexhalf  24855  xrhmeo  25247  pcoass  25325  ovoliunlem1  25803  ismbl2  25828  voliunlem2  25852  ioombl1lem4  25862  itg2ge0  26036  itg2addlem  26059  itgge0  26111  dvfsumrlimge0  26330  abelthlem1  26740  abelthlem2  26741  pilem2  26761  cos0pilt1  26842  rplogcl  26914  logge0  26915  argimgt0  26922  logdivlti  26930  logf1o2  26960  dvlog2lem  26962  ang180lem3  27121  atanlogaddlem  27223  atanlogsublem  27225  atantan  27233  atans2  27241  cxploglim2  27288  emcllem6  27310  emcllem7  27311  lgamgulmlem2  27339  ftalem1  27382  ftalem2  27383  ppinncl  27483  chtrpcl  27484  vmalelog  27514  chtub  27521  logfacubnd  27530  logfacbnd3  27532  logfacrlim  27533  logexprlim  27534  mersenne  27536  perfectlem2  27539  bpos1lem  27591  bposlem1  27593  bposlem2  27594  bposlem3  27595  bposlem4  27596  bposlem5  27597  bposlem6  27598  lgseisen  27688  lgsquadlem1  27689  chebbnd1lem1  27778  chebbnd1lem3  27780  rpvmasumlem  27796  dchrvmasumlem2  27807  dchrvmasumlema  27809  dchrvmasumiflem1  27810  dchrisum0flblem2  27818  dchrisum0fno1  27820  dchrisum0re  27822  dirith2  27837  logdivsum  27842  mulog2sumlem1  27843  mulog2sumlem2  27844  log2sumbnd  27853  chpdifbndlem1  27862  chpdifbndlem2  27863  logdivbnd  27865  selberg3lem1  27866  pntpbnd1a  27894  pntpbnd2  27896  pntibndlem3  27901  pntlemn  27909  pntlemj  27912  pntlemk  27915  pnt  27923  flt4lem7  27971  fltoprmlem2  27976  addsgt0d  28382  ltmulnegs1d  28544  absmuls  28612  abssge0  28613  leabss  28616  nnsge1  28711  bdayfinbndlem1  28835  tgldimor  28947  axlowdim  29521  minvecolem4  31464  abrexctf  33291  nndiffz1  33360  wrdt2ind  33498  xrge0addgt0  33560  elrgspnlem2  33786  ply1coedeg  34103  drngdimgt0  34232  extdgfialglem2  34307  cos9thpiminplylem1  34396  esumcvg2  34701  inelcarsg  34926  carsgclctunlem2  34934  signsply0  35163  signsvtn  35196  erdsze2lem2  35938  lcmineqlem23  43069  lcmineqlem  43070  aks4d1p1p6  43091  aks4d1p1  43094  aks5lem2  43205  pellqrex  43839  reglogltb  43851  reglogleb  43852  rmspecnonsq  43867  rmspecpos  43876  areaquad  44176  hashnzfz2  45264  binomcxplemdvbinom  45296  binomcxplemnotnn0  45299  fmul01  46536  climconstmpt  46612  stoweidlem26  46980  stoweidlem44  46998  stoweidlem45  46999  wallispilem3  47021  wallispi  47024  stirlinglem11  47038  dirkertrigeqlem1  47052  dirkertrigeqlem3  47054  fourierdlem80  47140  fourierdlem102  47162  fourierdlem107  47167  fourierdlem114  47174  etransclem46  47234  fmtnoge3  48559  fmtno4prmfac  48601  perfectALTVlem2  48764  gboge9  48806  mogoldbb  48827  tgoldbach  48859  gpg3kgrtriexlem3  49127  gpg3kgrtriexlem6  49130  nnolog2flm1  49646