Theorem eqbrtrrid 5143

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  enpr1g  8994  undom  9029  fidomdm  9285  prdom2  9959  infdju1  10143  infdif  10161  cfslb2n  10221  fin56  10346  dmct  10477  gchxpidm  10622  rankcf  10730  r1tskina  10735  tskuni  10736  ltsonq  10922  addgt0  11664  addgegt0  11665  addgtge0  11666  addge0  11667  expge1  14064  fsumrlim  15777  isumsup  15813  climcndslem1  15815  fprodge1  15961  3dvds  16301  bitsinv1lem  16411  phicl2  16738  frgpnabllem1  19803  lt6abl  19825  pgpfaclem2  20014  unitmulcl  20289  xrsdsreclblem  21329  znidomb  21471  lindfres  21732  gsumply1eq  22196  2ndcdisj2  23344  hmphindis  23684  tsms0  24029  tgptsmscls  24037  metustexhalf  24444  xrhmeo  24844  pcoass  24924  ovoliunlem1  25403  ismbl2  25428  voliunlem2  25452  ioombl1lem4  25462  itg2ge0  25636  itg2addlem  25659  itgge0  25712  dvfsumrlimge0  25937  abelthlem1  26341  abelthlem2  26342  pilem2  26362  cos0pilt1  26441  rplogcl  26513  logge0  26514  argimgt0  26521  logdivlti  26529  logf1o2  26559  dvlog2lem  26561  ang180lem3  26721  atanlogaddlem  26823  atanlogsublem  26825  atantan  26833  atans2  26841  cxploglim2  26889  emcllem6  26911  emcllem7  26912  lgamgulmlem2  26940  ftalem1  26983  ftalem2  26984  ppinncl  27084  chtrpcl  27085  vmalelog  27116  chtub  27123  logfacubnd  27132  logfacbnd3  27134  logfacrlim  27135  logexprlim  27136  mersenne  27138  perfectlem2  27141  bpos1lem  27193  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  lgseisen  27290  lgsquadlem1  27291  chebbnd1lem1  27380  chebbnd1lem3  27382  rpvmasumlem  27398  dchrvmasumlem2  27409  dchrvmasumlema  27411  dchrvmasumiflem1  27412  dchrisum0flblem2  27420  dchrisum0fno1  27422  dchrisum0re  27424  dirith2  27439  logdivsum  27444  mulog2sumlem1  27445  mulog2sumlem2  27446  log2sumbnd  27455  chpdifbndlem1  27464  chpdifbndlem2  27465  logdivbnd  27467  selberg3lem1  27468  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem3  27503  pntlemn  27511  pntlemj  27514  pntlemk  27517  pnt  27525  addsgt0d  27921  sltmulneg1d  28079  absmuls  28146  abssge0  28147  sleabs  28150  nnsge1  28235  tgldimor  28429  axlowdim  28888  minvecolem4  30809  abrexct  32640  abrexctf  32642  nndiffz1  32709  wrdt2ind  32875  xrge0addgt0  32958  elrgspnlem2  33194  drngdimgt0  33614  cos9thpiminplylem1  33772  esumcvg2  34077  inelcarsg  34302  carsgclctunlem2  34310  signsply0  34542  signsvtn  34575  erdsze2lem2  35191  lcmineqlem23  42039  lcmineqlem  42040  aks4d1p1p6  42061  aks4d1p1  42064  aks5lem2  42175  flt4lem7  42647  pellqrex  42867  reglogltb  42879  reglogleb  42880  rmspecnonsq  42895  rmspecpos  42905  areaquad  43205  hashnzfz2  44310  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  fmul01  45578  climconstmpt  45656  stoweidlem26  46024  stoweidlem44  46042  stoweidlem45  46043  wallispilem3  46065  wallispi  46068  stirlinglem11  46082  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  fourierdlem80  46184  fourierdlem102  46206  fourierdlem107  46211  fourierdlem114  46218  etransclem46  46278  fmtnoge3  47531  fmtno4prmfac  47573  perfectALTVlem2  47723  gboge9  47765  mogoldbb  47786  tgoldbach  47818  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem6  48079  nnolog2flm1  48579