Theorem eqbrtrrid 5136

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  enpr1g  8972  undom  9005  fidomdm  9246  prdom2  9928  infdju1  10112  infdif  10130  cfslb2n  10190  fin56  10315  dmct  10446  gchxpidm  10592  rankcf  10700  r1tskina  10705  tskuni  10706  ltsonq  10892  addgt0  11635  addgegt0  11636  addgtge0  11637  addge0  11638  expge1  14034  fsumrlim  15746  isumsup  15782  climcndslem1  15784  fprodge1  15930  3dvds  16270  bitsinv1lem  16380  phicl2  16707  frgpnabllem1  19814  lt6abl  19836  pgpfaclem2  20025  unitmulcl  20328  xrsdsreclblem  21379  znidomb  21528  lindfres  21790  gsumply1eq  22265  2ndcdisj2  23413  hmphindis  23753  tsms0  24098  tgptsmscls  24106  metustexhalf  24512  xrhmeo  24912  pcoass  24992  ovoliunlem1  25471  ismbl2  25496  voliunlem2  25520  ioombl1lem4  25530  itg2ge0  25704  itg2addlem  25727  itgge0  25780  dvfsumrlimge0  26005  abelthlem1  26409  abelthlem2  26410  pilem2  26430  cos0pilt1  26509  rplogcl  26581  logge0  26582  argimgt0  26589  logdivlti  26597  logf1o2  26627  dvlog2lem  26629  ang180lem3  26789  atanlogaddlem  26891  atanlogsublem  26893  atantan  26901  atans2  26909  cxploglim2  26957  emcllem6  26979  emcllem7  26980  lgamgulmlem2  27008  ftalem1  27051  ftalem2  27052  ppinncl  27152  chtrpcl  27153  vmalelog  27184  chtub  27191  logfacubnd  27200  logfacbnd3  27202  logfacrlim  27203  logexprlim  27204  mersenne  27206  perfectlem2  27209  bpos1lem  27261  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem4  27266  bposlem5  27267  bposlem6  27268  lgseisen  27358  lgsquadlem1  27359  chebbnd1lem1  27448  chebbnd1lem3  27450  rpvmasumlem  27466  dchrvmasumlem2  27477  dchrvmasumlema  27479  dchrvmasumiflem1  27480  dchrisum0flblem2  27488  dchrisum0fno1  27490  dchrisum0re  27492  dirith2  27507  logdivsum  27512  mulog2sumlem1  27513  mulog2sumlem2  27514  log2sumbnd  27523  chpdifbndlem1  27532  chpdifbndlem2  27533  logdivbnd  27535  selberg3lem1  27536  pntpbnd1a  27564  pntpbnd2  27566  pntibndlem3  27571  pntlemn  27579  pntlemj  27582  pntlemk  27585  pnt  27593  addsgt0d  28022  ltmulnegs1d  28184  absmuls  28252  abssge0  28253  leabss  28256  nnsge1  28351  bdayfinbndlem1  28475  tgldimor  28586  axlowdim  29046  minvecolem4  30967  abrexct  32804  abrexctf  32806  nndiffz1  32876  wrdt2ind  33045  xrge0addgt0  33109  elrgspnlem2  33336  ply1coedeg  33681  drngdimgt0  33795  extdgfialglem2  33870  cos9thpiminplylem1  33959  esumcvg2  34264  inelcarsg  34488  carsgclctunlem2  34496  signsply0  34728  signsvtn  34761  erdsze2lem2  35417  lcmineqlem23  42418  lcmineqlem  42419  aks4d1p1p6  42440  aks4d1p1  42443  aks5lem2  42554  flt4lem7  43014  pellqrex  43233  reglogltb  43245  reglogleb  43246  rmspecnonsq  43261  rmspecpos  43270  areaquad  43570  hashnzfz2  44674  binomcxplemdvbinom  44706  binomcxplemnotnn0  44709  fmul01  45937  climconstmpt  46013  stoweidlem26  46381  stoweidlem44  46399  stoweidlem45  46400  wallispilem3  46422  wallispi  46425  stirlinglem11  46439  dirkertrigeqlem1  46453  dirkertrigeqlem3  46455  fourierdlem80  46541  fourierdlem102  46563  fourierdlem107  46568  fourierdlem114  46575  etransclem46  46635  fmtnoge3  47887  fmtno4prmfac  47929  perfectALTVlem2  48079  gboge9  48121  mogoldbb  48142  tgoldbach  48174  gpg3kgrtriexlem3  48442  gpg3kgrtriexlem6  48445  nnolog2flm1  48947