Theorem eqbrtrrid 5133

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 5130	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1559   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  enpr1g  8997  undom  9030  fidomdm  9270  resfifsupp  9336  prdom2  9955  infdju1  10139  infdif  10157  cfslb2n  10218  fin56  10343  dmct  10474  gchxpidm  10620  rankcf  10728  r1tskina  10733  tskuni  10734  ltsonq  10920  addgt0  11666  addgegt0  11667  addgtge0  11668  addge0  11669  expge1  14105  fsumrlim  15829  isumsup  15867  climcndslem1  15869  fprodge1  16015  3dvds  16355  bitsinv1lem  16465  phicl2  16793  frgpnabllem1  19903  lt6abl  19925  pgpfaclem2  20114  unitmulcl  20415  xrsdsreclblem  21452  znidomb  21600  lindfres  21862  gsumply1eq  22359  2ndcdisj2  23504  hmphindis  23844  tsms0  24189  tgptsmscls  24197  metustexhalf  24603  xrhmeo  24995  pcoass  25073  ovoliunlem1  25551  ismbl2  25576  voliunlem2  25600  ioombl1lem4  25610  itg2ge0  25784  itg2addlem  25807  itgge0  25860  dvfsumrlimge0  26079  abelthlem1  26481  abelthlem2  26482  pilem2  26502  cos0pilt1  26584  rplogcl  26656  logge0  26657  argimgt0  26664  logdivlti  26672  logf1o2  26702  dvlog2lem  26704  ang180lem3  26863  atanlogaddlem  26965  atanlogsublem  26967  atantan  26975  atans2  26983  cxploglim2  27030  emcllem6  27052  emcllem7  27053  lgamgulmlem2  27081  ftalem1  27124  ftalem2  27125  ppinncl  27225  chtrpcl  27226  vmalelog  27256  chtub  27263  logfacubnd  27272  logfacbnd3  27274  logfacrlim  27275  logexprlim  27276  mersenne  27278  perfectlem2  27281  bpos1lem  27333  bposlem1  27335  bposlem2  27336  bposlem3  27337  bposlem4  27338  bposlem5  27339  bposlem6  27340  lgseisen  27430  lgsquadlem1  27431  chebbnd1lem1  27520  chebbnd1lem3  27522  rpvmasumlem  27538  dchrvmasumlem2  27549  dchrvmasumlema  27551  dchrvmasumiflem1  27552  dchrisum0flblem2  27560  dchrisum0fno1  27562  dchrisum0re  27564  dirith2  27579  logdivsum  27584  mulog2sumlem1  27585  mulog2sumlem2  27586  log2sumbnd  27595  chpdifbndlem1  27604  chpdifbndlem2  27605  logdivbnd  27607  selberg3lem1  27608  pntpbnd1a  27636  pntpbnd2  27638  pntibndlem3  27643  pntlemn  27651  pntlemj  27654  pntlemk  27657  pnt  27665  addsgt0d  28094  ltmulnegs1d  28256  absmuls  28324  abssge0  28325  leabss  28328  nnsge1  28423  bdayfinbndlem1  28547  tgldimor  28658  axlowdim  29118  minvecolem4  31039  abrexct  32877  abrexctf  32879  nndiffz1  32948  wrdt2ind  33091  xrge0addgt0  33155  elrgspnlem2  33384  ply1coedeg  33745  drngdimgt0  33875  extdgfialglem2  33950  cos9thpiminplylem1  34039  esumcvg2  34344  inelcarsg  34568  carsgclctunlem2  34576  signsply0  34805  signsvtn  34838  erdsze2lem2  35514  lcmineqlem23  42628  lcmineqlem  42629  aks4d1p1p6  42650  aks4d1p1  42653  aks5lem2  42764  flt4lem7  43201  pellqrex  43416  reglogltb  43428  reglogleb  43429  rmspecnonsq  43444  rmspecpos  43453  areaquad  43753  hashnzfz2  44857  binomcxplemdvbinom  44889  binomcxplemnotnn0  44892  fmul01  46116  climconstmpt  46192  stoweidlem26  46560  stoweidlem44  46578  stoweidlem45  46579  wallispilem3  46601  wallispi  46604  stirlinglem11  46618  dirkertrigeqlem1  46632  dirkertrigeqlem3  46634  fourierdlem80  46720  fourierdlem102  46742  fourierdlem107  46747  fourierdlem114  46754  etransclem46  46814  fmtnoge3  48099  fmtno4prmfac  48141  perfectALTVlem2  48304  gboge9  48346  mogoldbb  48367  tgoldbach  48399  gpg3kgrtriexlem3  48667  gpg3kgrtriexlem6  48670  nnolog2flm1  49172