Theorem eqbrtrrid 5160

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  enpr1g  9042  undom  9078  undomOLD  9079  fidomdm  9351  prdom2  10025  infdju1  10209  infdif  10227  cfslb2n  10287  fin56  10412  dmct  10543  gchxpidm  10688  rankcf  10796  r1tskina  10801  tskuni  10802  ltsonq  10988  addgt0  11728  addgegt0  11729  addgtge0  11730  addge0  11731  expge1  14122  fsumrlim  15832  isumsup  15868  climcndslem1  15870  fprodge1  16016  3dvds  16355  bitsinv1lem  16465  phicl2  16792  frgpnabllem1  19859  lt6abl  19881  pgpfaclem2  20070  unitmulcl  20345  xrsdsreclblem  21385  znidomb  21527  lindfres  21788  gsumply1eq  22252  2ndcdisj2  23400  hmphindis  23740  tsms0  24085  tgptsmscls  24093  metustexhalf  24500  xrhmeo  24900  pcoass  24980  ovoliunlem1  25460  ismbl2  25485  voliunlem2  25509  ioombl1lem4  25519  itg2ge0  25693  itg2addlem  25716  itgge0  25769  dvfsumrlimge0  25994  abelthlem1  26398  abelthlem2  26399  pilem2  26419  cos0pilt1  26498  rplogcl  26570  logge0  26571  argimgt0  26578  logdivlti  26586  logf1o2  26616  dvlog2lem  26618  ang180lem3  26778  atanlogaddlem  26880  atanlogsublem  26882  atantan  26890  atans2  26898  cxploglim2  26946  emcllem6  26968  emcllem7  26969  lgamgulmlem2  26997  ftalem1  27040  ftalem2  27041  ppinncl  27141  chtrpcl  27142  vmalelog  27173  chtub  27180  logfacubnd  27189  logfacbnd3  27191  logfacrlim  27192  logexprlim  27193  mersenne  27195  perfectlem2  27198  bpos1lem  27250  bposlem1  27252  bposlem2  27253  bposlem3  27254  bposlem4  27255  bposlem5  27256  bposlem6  27257  lgseisen  27347  lgsquadlem1  27348  chebbnd1lem1  27437  chebbnd1lem3  27439  rpvmasumlem  27455  dchrvmasumlem2  27466  dchrvmasumlema  27468  dchrvmasumiflem1  27469  dchrisum0flblem2  27477  dchrisum0fno1  27479  dchrisum0re  27481  dirith2  27496  logdivsum  27501  mulog2sumlem1  27502  mulog2sumlem2  27503  log2sumbnd  27512  chpdifbndlem1  27521  chpdifbndlem2  27522  logdivbnd  27524  selberg3lem1  27525  pntpbnd1a  27553  pntpbnd2  27555  pntibndlem3  27560  pntlemn  27568  pntlemj  27571  pntlemk  27574  pnt  27582  addsgt0d  27978  sltmulneg1d  28136  absmuls  28203  abssge0  28204  sleabs  28207  nnsge1  28292  tgldimor  28486  axlowdim  28945  minvecolem4  30866  abrexct  32699  abrexctf  32701  nndiffz1  32768  wrdt2ind  32934  xrge0addgt0  33017  elrgspnlem2  33243  drngdimgt0  33663  cos9thpiminplylem1  33821  esumcvg2  34123  inelcarsg  34348  carsgclctunlem2  34356  signsply0  34588  signsvtn  34621  erdsze2lem2  35231  lcmineqlem23  42069  lcmineqlem  42070  aks4d1p1p6  42091  aks4d1p1  42094  aks5lem2  42205  flt4lem7  42657  pellqrex  42877  reglogltb  42889  reglogleb  42890  rmspecnonsq  42905  rmspecpos  42915  areaquad  43215  hashnzfz2  44320  binomcxplemdvbinom  44352  binomcxplemnotnn0  44355  fmul01  45589  climconstmpt  45667  stoweidlem26  46035  stoweidlem44  46053  stoweidlem45  46054  wallispilem3  46076  wallispi  46079  stirlinglem11  46093  dirkertrigeqlem1  46107  dirkertrigeqlem3  46109  fourierdlem80  46195  fourierdlem102  46217  fourierdlem107  46222  fourierdlem114  46229  etransclem46  46289  fmtnoge3  47524  fmtno4prmfac  47566  perfectALTVlem2  47716  gboge9  47758  mogoldbb  47779  tgoldbach  47811  gpg3kgrtriexlem3  48067  gpg3kgrtriexlem6  48070  nnolog2flm1  48550