Theorem eqbrtrrid 5122

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

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  enpr1g  8963  undom  8996  fidomdm  9237  prdom2  9919  infdju1  10103  infdif  10121  cfslb2n  10181  fin56  10306  dmct  10437  gchxpidm  10583  rankcf  10691  r1tskina  10696  tskuni  10697  ltsonq  10883  addgt0  11627  addgegt0  11628  addgtge0  11629  addge0  11630  expge1  14052  fsumrlim  15765  isumsup  15803  climcndslem1  15805  fprodge1  15951  3dvds  16291  bitsinv1lem  16401  phicl2  16729  frgpnabllem1  19839  lt6abl  19861  pgpfaclem2  20050  unitmulcl  20351  xrsdsreclblem  21402  znidomb  21551  lindfres  21813  gsumply1eq  22284  2ndcdisj2  23432  hmphindis  23772  tsms0  24117  tgptsmscls  24125  metustexhalf  24531  xrhmeo  24923  pcoass  25001  ovoliunlem1  25479  ismbl2  25504  voliunlem2  25528  ioombl1lem4  25538  itg2ge0  25712  itg2addlem  25735  itgge0  25788  dvfsumrlimge0  26007  abelthlem1  26409  abelthlem2  26410  pilem2  26430  cos0pilt1  26509  rplogcl  26581  logge0  26582  argimgt0  26589  logdivlti  26597  logf1o2  26627  dvlog2lem  26629  ang180lem3  26788  atanlogaddlem  26890  atanlogsublem  26892  atantan  26900  atans2  26908  cxploglim2  26956  emcllem6  26978  emcllem7  26979  lgamgulmlem2  27007  ftalem1  27050  ftalem2  27051  ppinncl  27151  chtrpcl  27152  vmalelog  27182  chtub  27189  logfacubnd  27198  logfacbnd3  27200  logfacrlim  27201  logexprlim  27202  mersenne  27204  perfectlem2  27207  bpos1lem  27259  bposlem1  27261  bposlem2  27262  bposlem3  27263  bposlem4  27264  bposlem5  27265  bposlem6  27266  lgseisen  27356  lgsquadlem1  27357  chebbnd1lem1  27446  chebbnd1lem3  27448  rpvmasumlem  27464  dchrvmasumlem2  27475  dchrvmasumlema  27477  dchrvmasumiflem1  27478  dchrisum0flblem2  27486  dchrisum0fno1  27488  dchrisum0re  27490  dirith2  27505  logdivsum  27510  mulog2sumlem1  27511  mulog2sumlem2  27512  log2sumbnd  27521  chpdifbndlem1  27530  chpdifbndlem2  27531  logdivbnd  27533  selberg3lem1  27534  pntpbnd1a  27562  pntpbnd2  27564  pntibndlem3  27569  pntlemn  27577  pntlemj  27580  pntlemk  27583  pnt  27591  addsgt0d  28020  ltmulnegs1d  28182  absmuls  28250  abssge0  28251  leabss  28254  nnsge1  28349  bdayfinbndlem1  28473  tgldimor  28584  axlowdim  29044  minvecolem4  30966  abrexct  32803  abrexctf  32805  nndiffz1  32874  wrdt2ind  33028  xrge0addgt0  33092  elrgspnlem2  33319  ply1coedeg  33664  drngdimgt0  33778  extdgfialglem2  33853  cos9thpiminplylem1  33942  esumcvg2  34247  inelcarsg  34471  carsgclctunlem2  34479  signsply0  34711  signsvtn  34744  erdsze2lem2  35402  lcmineqlem23  42504  lcmineqlem  42505  aks4d1p1p6  42526  aks4d1p1  42529  aks5lem2  42640  flt4lem7  43106  pellqrex  43325  reglogltb  43337  reglogleb  43338  rmspecnonsq  43353  rmspecpos  43362  areaquad  43662  hashnzfz2  44766  binomcxplemdvbinom  44798  binomcxplemnotnn0  44801  fmul01  46028  climconstmpt  46104  stoweidlem26  46472  stoweidlem44  46490  stoweidlem45  46491  wallispilem3  46513  wallispi  46516  stirlinglem11  46530  dirkertrigeqlem1  46544  dirkertrigeqlem3  46546  fourierdlem80  46632  fourierdlem102  46654  fourierdlem107  46659  fourierdlem114  46666  etransclem46  46726  fmtnoge3  48005  fmtno4prmfac  48047  perfectALTVlem2  48210  gboge9  48252  mogoldbb  48273  tgoldbach  48305  gpg3kgrtriexlem3  48573  gpg3kgrtriexlem6  48576  nnolog2flm1  49078