Theorem eqbrtrrid 5131

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  enpr1g  8954  undom  8987  fidomdm  9227  prdom2  9906  infdju1  10090  infdif  10108  cfslb2n  10168  fin56  10293  dmct  10424  gchxpidm  10569  rankcf  10677  r1tskina  10682  tskuni  10683  ltsonq  10869  addgt0  11612  addgegt0  11613  addgtge0  11614  addge0  11615  expge1  14010  fsumrlim  15722  isumsup  15758  climcndslem1  15760  fprodge1  15906  3dvds  16246  bitsinv1lem  16356  phicl2  16683  frgpnabllem1  19789  lt6abl  19811  pgpfaclem2  20000  unitmulcl  20302  xrsdsreclblem  21353  znidomb  21502  lindfres  21764  gsumply1eq  22227  2ndcdisj2  23375  hmphindis  23715  tsms0  24060  tgptsmscls  24068  metustexhalf  24474  xrhmeo  24874  pcoass  24954  ovoliunlem1  25433  ismbl2  25458  voliunlem2  25482  ioombl1lem4  25492  itg2ge0  25666  itg2addlem  25689  itgge0  25742  dvfsumrlimge0  25967  abelthlem1  26371  abelthlem2  26372  pilem2  26392  cos0pilt1  26471  rplogcl  26543  logge0  26544  argimgt0  26551  logdivlti  26559  logf1o2  26589  dvlog2lem  26591  ang180lem3  26751  atanlogaddlem  26853  atanlogsublem  26855  atantan  26863  atans2  26871  cxploglim2  26919  emcllem6  26941  emcllem7  26942  lgamgulmlem2  26970  ftalem1  27013  ftalem2  27014  ppinncl  27114  chtrpcl  27115  vmalelog  27146  chtub  27153  logfacubnd  27162  logfacbnd3  27164  logfacrlim  27165  logexprlim  27166  mersenne  27168  perfectlem2  27171  bpos1lem  27223  bposlem1  27225  bposlem2  27226  bposlem3  27227  bposlem4  27228  bposlem5  27229  bposlem6  27230  lgseisen  27320  lgsquadlem1  27321  chebbnd1lem1  27410  chebbnd1lem3  27412  rpvmasumlem  27428  dchrvmasumlem2  27439  dchrvmasumlema  27441  dchrvmasumiflem1  27442  dchrisum0flblem2  27450  dchrisum0fno1  27452  dchrisum0re  27454  dirith2  27469  logdivsum  27474  mulog2sumlem1  27475  mulog2sumlem2  27476  log2sumbnd  27485  chpdifbndlem1  27494  chpdifbndlem2  27495  logdivbnd  27497  selberg3lem1  27498  pntpbnd1a  27526  pntpbnd2  27528  pntibndlem3  27533  pntlemn  27541  pntlemj  27544  pntlemk  27547  pnt  27555  addsgt0d  27960  sltmulneg1d  28118  absmuls  28185  abssge0  28186  sleabs  28189  nnsge1  28274  tgldimor  28483  axlowdim  28943  minvecolem4  30864  abrexct  32704  abrexctf  32706  nndiffz1  32775  wrdt2ind  32943  xrge0addgt0  33007  elrgspnlem2  33219  drngdimgt0  33654  extdgfialglem2  33729  cos9thpiminplylem1  33818  esumcvg2  34123  inelcarsg  34347  carsgclctunlem2  34355  signsply0  34587  signsvtn  34620  erdsze2lem2  35271  lcmineqlem23  42167  lcmineqlem  42168  aks4d1p1p6  42189  aks4d1p1  42192  aks5lem2  42303  flt4lem7  42780  pellqrex  42999  reglogltb  43011  reglogleb  43012  rmspecnonsq  43027  rmspecpos  43036  areaquad  43336  hashnzfz2  44441  binomcxplemdvbinom  44473  binomcxplemnotnn0  44476  fmul01  45707  climconstmpt  45783  stoweidlem26  46151  stoweidlem44  46169  stoweidlem45  46170  wallispilem3  46192  wallispi  46195  stirlinglem11  46209  dirkertrigeqlem1  46223  dirkertrigeqlem3  46225  fourierdlem80  46311  fourierdlem102  46333  fourierdlem107  46338  fourierdlem114  46345  etransclem46  46405  fmtnoge3  47657  fmtno4prmfac  47699  perfectALTVlem2  47849  gboge9  47891  mogoldbb  47912  tgoldbach  47944  gpg3kgrtriexlem3  48212  gpg3kgrtriexlem6  48215  nnolog2flm1  48718