Theorem eqbrtrrid 5184

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  enpr1g  9022  undom  9061  undomOLD  9062  fidomdm  9331  prdom2  10003  infdju1  10186  infdif  10206  cfslb2n  10265  fin56  10390  dmct  10521  gchxpidm  10666  rankcf  10774  r1tskina  10779  tskuni  10780  ltsonq  10966  addgt0  11702  addgegt0  11703  addgtge0  11704  addge0  11705  expge1  14067  fsumrlim  15759  isumsup  15795  climcndslem1  15797  fprodge1  15941  3dvds  16276  bitsinv1lem  16384  phicl2  16703  frgpnabllem1  19743  lt6abl  19765  pgpfaclem2  19954  unitmulcl  20198  xrsdsreclblem  20997  znidomb  21123  lindfres  21384  gsumply1eq  21836  2ndcdisj2  22968  hmphindis  23308  tsms0  23653  tgptsmscls  23661  metustexhalf  24072  xrhmeo  24469  pcoass  24547  ovoliunlem1  25026  ismbl2  25051  voliunlem2  25075  ioombl1lem4  25085  itg2ge0  25260  itg2addlem  25283  itgge0  25335  dvfsumrlimge0  25554  abelthlem1  25950  abelthlem2  25951  pilem2  25971  cos0pilt1  26048  rplogcl  26119  logge0  26120  argimgt0  26127  logdivlti  26135  logf1o2  26165  dvlog2lem  26167  ang180lem3  26323  atanlogaddlem  26425  atanlogsublem  26427  atantan  26435  atans2  26443  cxploglim2  26490  emcllem6  26512  emcllem7  26513  lgamgulmlem2  26541  ftalem1  26584  ftalem2  26585  ppinncl  26685  chtrpcl  26686  vmalelog  26715  chtub  26722  logfacubnd  26731  logfacbnd3  26733  logfacrlim  26734  logexprlim  26735  mersenne  26737  perfectlem2  26740  bpos1lem  26792  bposlem1  26794  bposlem2  26795  bposlem3  26796  bposlem4  26797  bposlem5  26798  bposlem6  26799  lgseisen  26889  lgsquadlem1  26890  chebbnd1lem1  26979  chebbnd1lem3  26981  rpvmasumlem  26997  dchrvmasumlem2  27008  dchrvmasumlema  27010  dchrvmasumiflem1  27011  dchrisum0flblem2  27019  dchrisum0fno1  27021  dchrisum0re  27023  dirith2  27038  logdivsum  27043  mulog2sumlem1  27044  mulog2sumlem2  27045  log2sumbnd  27054  chpdifbndlem1  27063  chpdifbndlem2  27064  logdivbnd  27066  selberg3lem1  27067  pntpbnd1a  27095  pntpbnd2  27097  pntibndlem3  27102  pntlemn  27110  pntlemj  27113  pntlemk  27116  pnt  27124  sltmulneg1d  27638  tgldimor  27791  axlowdim  28257  minvecolem4  30171  abrexct  31979  abrexctf  31981  nndiffz1  32035  wrdt2ind  32155  xrge0addgt0  32230  drngdimgt0  32762  esumcvg2  33154  inelcarsg  33379  carsgclctunlem2  33387  signsply0  33631  signsvtn  33664  erdsze2lem2  34264  lcmineqlem23  41002  lcmineqlem  41003  aks4d1p1p6  41024  aks4d1p1  41027  metakunt2  41072  metakunt29  41099  2xp3dxp2ge1d  41108  flt4lem7  41483  pellqrex  41699  reglogltb  41711  reglogleb  41712  rmspecnonsq  41727  rmspecpos  41737  areaquad  42047  hashnzfz2  43162  binomcxplemdvbinom  43194  binomcxplemnotnn0  43197  fmul01  44375  climconstmpt  44453  stoweidlem26  44821  stoweidlem44  44839  stoweidlem45  44840  wallispilem3  44862  wallispi  44865  stirlinglem11  44879  dirkertrigeqlem1  44893  dirkertrigeqlem3  44895  fourierdlem80  44981  fourierdlem102  45003  fourierdlem107  45008  fourierdlem114  45015  etransclem46  45075  fmtnoge3  46277  fmtno4prmfac  46319  perfectALTVlem2  46469  gboge9  46511  mogoldbb  46532  tgoldbach  46564  nnolog2flm1  47354