Theorem eqbrtrrid 5178

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143

This theorem is referenced by:  enpr1g  9064  undom  9100  undomOLD  9101  fidomdm  9375  prdom2  10047  infdju1  10231  infdif  10249  cfslb2n  10309  fin56  10434  dmct  10565  gchxpidm  10710  rankcf  10818  r1tskina  10823  tskuni  10824  ltsonq  11010  addgt0  11750  addgegt0  11751  addgtge0  11752  addge0  11753  expge1  14141  fsumrlim  15848  isumsup  15884  climcndslem1  15886  fprodge1  16032  3dvds  16369  bitsinv1lem  16479  phicl2  16806  frgpnabllem1  19892  lt6abl  19914  pgpfaclem2  20103  unitmulcl  20381  xrsdsreclblem  21431  znidomb  21581  lindfres  21844  gsumply1eq  22314  2ndcdisj2  23466  hmphindis  23806  tsms0  24151  tgptsmscls  24159  metustexhalf  24570  xrhmeo  24978  pcoass  25058  ovoliunlem1  25538  ismbl2  25563  voliunlem2  25587  ioombl1lem4  25597  itg2ge0  25771  itg2addlem  25794  itgge0  25847  dvfsumrlimge0  26072  abelthlem1  26476  abelthlem2  26477  pilem2  26497  cos0pilt1  26575  rplogcl  26647  logge0  26648  argimgt0  26655  logdivlti  26663  logf1o2  26693  dvlog2lem  26695  ang180lem3  26855  atanlogaddlem  26957  atanlogsublem  26959  atantan  26967  atans2  26975  cxploglim2  27023  emcllem6  27045  emcllem7  27046  lgamgulmlem2  27074  ftalem1  27117  ftalem2  27118  ppinncl  27218  chtrpcl  27219  vmalelog  27250  chtub  27257  logfacubnd  27266  logfacbnd3  27268  logfacrlim  27269  logexprlim  27270  mersenne  27272  perfectlem2  27275  bpos1lem  27327  bposlem1  27329  bposlem2  27330  bposlem3  27331  bposlem4  27332  bposlem5  27333  bposlem6  27334  lgseisen  27424  lgsquadlem1  27425  chebbnd1lem1  27514  chebbnd1lem3  27516  rpvmasumlem  27532  dchrvmasumlem2  27543  dchrvmasumlema  27545  dchrvmasumiflem1  27546  dchrisum0flblem2  27554  dchrisum0fno1  27556  dchrisum0re  27558  dirith2  27573  logdivsum  27578  mulog2sumlem1  27579  mulog2sumlem2  27580  log2sumbnd  27589  chpdifbndlem1  27598  chpdifbndlem2  27599  logdivbnd  27601  selberg3lem1  27602  pntpbnd1a  27630  pntpbnd2  27632  pntibndlem3  27637  pntlemn  27645  pntlemj  27648  pntlemk  27651  pnt  27659  addsgt0d  28048  sltmulneg1d  28203  absmuls  28269  abssge0  28270  sleabs  28273  nnsge1  28347  tgldimor  28511  axlowdim  28977  minvecolem4  30900  abrexct  32729  abrexctf  32731  nndiffz1  32789  wrdt2ind  32939  xrge0addgt0  33023  elrgspnlem2  33248  drngdimgt0  33670  esumcvg2  34089  inelcarsg  34314  carsgclctunlem2  34322  signsply0  34567  signsvtn  34600  erdsze2lem2  35210  lcmineqlem23  42053  lcmineqlem  42054  aks4d1p1p6  42075  aks4d1p1  42078  aks5lem2  42189  metakunt2  42208  metakunt29  42235  2xp3dxp2ge1d  42243  flt4lem7  42674  pellqrex  42895  reglogltb  42907  reglogleb  42908  rmspecnonsq  42923  rmspecpos  42933  areaquad  43233  hashnzfz2  44345  binomcxplemdvbinom  44377  binomcxplemnotnn0  44380  fmul01  45600  climconstmpt  45678  stoweidlem26  46046  stoweidlem44  46064  stoweidlem45  46065  wallispilem3  46087  wallispi  46090  stirlinglem11  46104  dirkertrigeqlem1  46118  dirkertrigeqlem3  46120  fourierdlem80  46206  fourierdlem102  46228  fourierdlem107  46233  fourierdlem114  46240  etransclem46  46300  fmtnoge3  47522  fmtno4prmfac  47564  perfectALTVlem2  47714  gboge9  47756  mogoldbb  47777  tgoldbach  47809  gpg3kgrtriexlem3  48046  gpg3kgrtriexlem6  48049  nnolog2flm1  48516