Theorem eqbrtrrid 5184

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  enpr1g  9019  undom  9058  undomOLD  9059  fidomdm  9328  prdom2  10000  infdju1  10183  infdif  10203  cfslb2n  10262  fin56  10387  dmct  10518  gchxpidm  10663  rankcf  10771  r1tskina  10776  tskuni  10777  ltsonq  10963  addgt0  11699  addgegt0  11700  addgtge0  11701  addge0  11702  expge1  14064  fsumrlim  15756  isumsup  15792  climcndslem1  15794  fprodge1  15938  3dvds  16273  bitsinv1lem  16381  phicl2  16700  frgpnabllem1  19740  lt6abl  19762  pgpfaclem2  19951  unitmulcl  20193  xrsdsreclblem  20990  znidomb  21116  lindfres  21377  gsumply1eq  21828  2ndcdisj2  22960  hmphindis  23300  tsms0  23645  tgptsmscls  23653  metustexhalf  24064  xrhmeo  24461  pcoass  24539  ovoliunlem1  25018  ismbl2  25043  voliunlem2  25067  ioombl1lem4  25077  itg2ge0  25252  itg2addlem  25275  itgge0  25327  dvfsumrlimge0  25546  abelthlem1  25942  abelthlem2  25943  pilem2  25963  cos0pilt1  26040  rplogcl  26111  logge0  26112  argimgt0  26119  logdivlti  26127  logf1o2  26157  dvlog2lem  26159  ang180lem3  26313  atanlogaddlem  26415  atanlogsublem  26417  atantan  26425  atans2  26433  cxploglim2  26480  emcllem6  26502  emcllem7  26503  lgamgulmlem2  26531  ftalem1  26574  ftalem2  26575  ppinncl  26675  chtrpcl  26676  vmalelog  26705  chtub  26712  logfacubnd  26721  logfacbnd3  26723  logfacrlim  26724  logexprlim  26725  mersenne  26727  perfectlem2  26730  bpos1lem  26782  bposlem1  26784  bposlem2  26785  bposlem3  26786  bposlem4  26787  bposlem5  26788  bposlem6  26789  lgseisen  26879  lgsquadlem1  26880  chebbnd1lem1  26969  chebbnd1lem3  26971  rpvmasumlem  26987  dchrvmasumlem2  26998  dchrvmasumlema  27000  dchrvmasumiflem1  27001  dchrisum0flblem2  27009  dchrisum0fno1  27011  dchrisum0re  27013  dirith2  27028  logdivsum  27033  mulog2sumlem1  27034  mulog2sumlem2  27035  log2sumbnd  27044  chpdifbndlem1  27053  chpdifbndlem2  27054  logdivbnd  27056  selberg3lem1  27057  pntpbnd1a  27085  pntpbnd2  27087  pntibndlem3  27092  pntlemn  27100  pntlemj  27103  pntlemk  27106  pnt  27114  sltmulneg1d  27625  tgldimor  27750  axlowdim  28216  minvecolem4  30128  abrexct  31936  abrexctf  31938  nndiffz1  31992  wrdt2ind  32112  xrge0addgt0  32187  drngdimgt0  32698  esumcvg2  33080  inelcarsg  33305  carsgclctunlem2  33313  signsply0  33557  signsvtn  33590  erdsze2lem2  34190  lcmineqlem23  40911  lcmineqlem  40912  aks4d1p1p6  40933  aks4d1p1  40936  metakunt2  40981  metakunt29  41008  2xp3dxp2ge1d  41017  flt4lem7  41402  pellqrex  41607  reglogltb  41619  reglogleb  41620  rmspecnonsq  41635  rmspecpos  41645  areaquad  41955  hashnzfz2  43070  binomcxplemdvbinom  43102  binomcxplemnotnn0  43105  fmul01  44286  climconstmpt  44364  stoweidlem26  44732  stoweidlem44  44750  stoweidlem45  44751  wallispilem3  44773  wallispi  44776  stirlinglem11  44790  dirkertrigeqlem1  44804  dirkertrigeqlem3  44806  fourierdlem80  44892  fourierdlem102  44914  fourierdlem107  44919  fourierdlem114  44926  etransclem46  44986  fmtnoge3  46188  fmtno4prmfac  46230  perfectALTVlem2  46380  gboge9  46422  mogoldbb  46443  tgoldbach  46475  nnolog2flm1  47266