Theorem eqbrtrrid 5106

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  enpr1g  8764  undom  8800  fidomdm  9026  prdom2  9693  infdju1  9876  infdif  9896  cfslb2n  9955  fin56  10080  dmct  10211  gchxpidm  10356  rankcf  10464  r1tskina  10469  tskuni  10470  ltsonq  10656  addgt0  11391  addgegt0  11392  addgtge0  11393  addge0  11394  expge1  13748  fsumrlim  15451  isumsup  15487  climcndslem1  15489  fprodge1  15633  3dvds  15968  bitsinv1lem  16076  phicl2  16397  frgpnabllem1  19389  lt6abl  19411  pgpfaclem2  19600  unitmulcl  19821  xrsdsreclblem  20556  znidomb  20681  lindfres  20940  gsumply1eq  21386  2ndcdisj2  22516  hmphindis  22856  tsms0  23201  tgptsmscls  23209  metustexhalf  23618  xrhmeo  24015  pcoass  24093  ovoliunlem1  24571  ismbl2  24596  voliunlem2  24620  ioombl1lem4  24630  itg2ge0  24805  itg2addlem  24828  itgge0  24880  dvfsumrlimge0  25099  abelthlem1  25495  abelthlem2  25496  pilem2  25516  cos0pilt1  25593  rplogcl  25664  logge0  25665  argimgt0  25672  logdivlti  25680  logf1o2  25710  dvlog2lem  25712  ang180lem3  25866  atanlogaddlem  25968  atanlogsublem  25970  atantan  25978  atans2  25986  cxploglim2  26033  emcllem6  26055  emcllem7  26056  lgamgulmlem2  26084  ftalem1  26127  ftalem2  26128  ppinncl  26228  chtrpcl  26229  vmalelog  26258  chtub  26265  logfacubnd  26274  logfacbnd3  26276  logfacrlim  26277  logexprlim  26278  mersenne  26280  perfectlem2  26283  bpos1lem  26335  bposlem1  26337  bposlem2  26338  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem6  26342  lgseisen  26432  lgsquadlem1  26433  chebbnd1lem1  26522  chebbnd1lem3  26524  rpvmasumlem  26540  dchrvmasumlem2  26551  dchrvmasumlema  26553  dchrvmasumiflem1  26554  dchrisum0flblem2  26562  dchrisum0fno1  26564  dchrisum0re  26566  dirith2  26581  logdivsum  26586  mulog2sumlem1  26587  mulog2sumlem2  26588  log2sumbnd  26597  chpdifbndlem1  26606  chpdifbndlem2  26607  logdivbnd  26609  selberg3lem1  26610  pntpbnd1a  26638  pntpbnd2  26640  pntibndlem3  26645  pntlemn  26653  pntlemj  26656  pntlemk  26659  pnt  26667  tgldimor  26767  axlowdim  27232  minvecolem4  29143  abrexct  30953  abrexctf  30955  nndiffz1  31009  wrdt2ind  31127  xrge0addgt0  31202  drngdimgt0  31603  esumcvg2  31955  inelcarsg  32178  carsgclctunlem2  32186  signsply0  32430  signsvtn  32463  erdsze2lem2  33066  lcmineqlem23  39987  lcmineqlem  39988  aks4d1p1p6  40009  aks4d1p1  40012  metakunt2  40054  metakunt29  40081  2xp3dxp2ge1d  40090  flt4lem7  40412  pellqrex  40617  reglogltb  40629  reglogleb  40630  rmspecnonsq  40645  rmspecpos  40654  areaquad  40963  hashnzfz2  41828  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  fmul01  43011  climconstmpt  43089  stoweidlem26  43457  stoweidlem44  43475  stoweidlem45  43476  wallispilem3  43498  wallispi  43501  stirlinglem11  43515  dirkertrigeqlem1  43529  dirkertrigeqlem3  43531  fourierdlem80  43617  fourierdlem102  43639  fourierdlem107  43644  fourierdlem114  43651  etransclem46  43711  fmtnoge3  44870  fmtno4prmfac  44912  perfectALTVlem2  45062  gboge9  45104  mogoldbb  45125  tgoldbach  45157  nnolog2flm1  45824