Theorem eqbrtrrid 5134

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  enpr1g  8960  undom  8993  fidomdm  9234  prdom2  9916  infdju1  10100  infdif  10118  cfslb2n  10178  fin56  10303  dmct  10434  gchxpidm  10580  rankcf  10688  r1tskina  10693  tskuni  10694  ltsonq  10880  addgt0  11623  addgegt0  11624  addgtge0  11625  addge0  11626  expge1  14022  fsumrlim  15734  isumsup  15770  climcndslem1  15772  fprodge1  15918  3dvds  16258  bitsinv1lem  16368  phicl2  16695  frgpnabllem1  19802  lt6abl  19824  pgpfaclem2  20013  unitmulcl  20316  xrsdsreclblem  21367  znidomb  21516  lindfres  21778  gsumply1eq  22253  2ndcdisj2  23401  hmphindis  23741  tsms0  24086  tgptsmscls  24094  metustexhalf  24500  xrhmeo  24900  pcoass  24980  ovoliunlem1  25459  ismbl2  25484  voliunlem2  25508  ioombl1lem4  25518  itg2ge0  25692  itg2addlem  25715  itgge0  25768  dvfsumrlimge0  25993  abelthlem1  26397  abelthlem2  26398  pilem2  26418  cos0pilt1  26497  rplogcl  26569  logge0  26570  argimgt0  26577  logdivlti  26585  logf1o2  26615  dvlog2lem  26617  ang180lem3  26777  atanlogaddlem  26879  atanlogsublem  26881  atantan  26889  atans2  26897  cxploglim2  26945  emcllem6  26967  emcllem7  26968  lgamgulmlem2  26996  ftalem1  27039  ftalem2  27040  ppinncl  27140  chtrpcl  27141  vmalelog  27172  chtub  27179  logfacubnd  27188  logfacbnd3  27190  logfacrlim  27191  logexprlim  27192  mersenne  27194  perfectlem2  27197  bpos1lem  27249  bposlem1  27251  bposlem2  27252  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  lgseisen  27346  lgsquadlem1  27347  chebbnd1lem1  27436  chebbnd1lem3  27438  rpvmasumlem  27454  dchrvmasumlem2  27465  dchrvmasumlema  27467  dchrvmasumiflem1  27468  dchrisum0flblem2  27476  dchrisum0fno1  27478  dchrisum0re  27480  dirith2  27495  logdivsum  27500  mulog2sumlem1  27501  mulog2sumlem2  27502  log2sumbnd  27511  chpdifbndlem1  27520  chpdifbndlem2  27521  logdivbnd  27523  selberg3lem1  27524  pntpbnd1a  27552  pntpbnd2  27554  pntibndlem3  27559  pntlemn  27567  pntlemj  27570  pntlemk  27573  pnt  27581  addsgt0d  28010  ltmulnegs1d  28172  absmuls  28240  abssge0  28241  leabss  28244  nnsge1  28339  bdayfinbndlem1  28463  tgldimor  28574  axlowdim  29034  minvecolem4  30955  abrexct  32794  abrexctf  32796  nndiffz1  32866  wrdt2ind  33035  xrge0addgt0  33099  elrgspnlem2  33325  ply1coedeg  33670  drngdimgt0  33775  extdgfialglem2  33850  cos9thpiminplylem1  33939  esumcvg2  34244  inelcarsg  34468  carsgclctunlem2  34476  signsply0  34708  signsvtn  34741  erdsze2lem2  35398  lcmineqlem23  42305  lcmineqlem  42306  aks4d1p1p6  42327  aks4d1p1  42330  aks5lem2  42441  flt4lem7  42902  pellqrex  43121  reglogltb  43133  reglogleb  43134  rmspecnonsq  43149  rmspecpos  43158  areaquad  43458  hashnzfz2  44562  binomcxplemdvbinom  44594  binomcxplemnotnn0  44597  fmul01  45826  climconstmpt  45902  stoweidlem26  46270  stoweidlem44  46288  stoweidlem45  46289  wallispilem3  46311  wallispi  46314  stirlinglem11  46328  dirkertrigeqlem1  46342  dirkertrigeqlem3  46344  fourierdlem80  46430  fourierdlem102  46452  fourierdlem107  46457  fourierdlem114  46464  etransclem46  46524  fmtnoge3  47776  fmtno4prmfac  47818  perfectALTVlem2  47968  gboge9  48010  mogoldbb  48031  tgoldbach  48063  gpg3kgrtriexlem3  48331  gpg3kgrtriexlem6  48334  nnolog2flm1  48836