Theorem eqbrtrrid 5145

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  enpr1g  9033  undom  9067  fidomdm  9305  resfifsupp  9371  prdom2  10013  infdju1  10196  infdif  10214  cfslb2n  10274  fin56  10399  dmct  10530  dmctOLD  10531  gchxpidm  10682  rankcf  10790  r1tskina  10795  tskuni  10796  ltsonq  10982  addgt0  11728  addgegt0  11729  addgtge0  11730  addge0  11731  expge1  14167  fsumrlim  15902  isumsup  15940  climcndslem1  15942  fprodge1  16088  3dvds  16427  bitsinv1lem  16537  phicl2  16865  frgpnabllem1  20006  lt6abl  20028  pgpfaclem2  20217  unitmulcl  20527  xrsdsreclblem  21632  znidomb  21780  lindfres  22042  gsumply1eq  22540  abrexct  23686  2ndcdisj2  23689  hmphindis  24029  tsms0  24374  tgptsmscls  24382  metustexhalf  24788  xrhmeo  25180  pcoass  25258  ovoliunlem1  25736  ismbl2  25761  voliunlem2  25785  ioombl1lem4  25795  itg2ge0  25969  itg2addlem  25992  itgge0  26045  dvfsumrlimge0  26264  abelthlem1  26674  abelthlem2  26675  pilem2  26695  cos0pilt1  26777  rplogcl  26849  logge0  26850  argimgt0  26857  logdivlti  26865  logf1o2  26895  dvlog2lem  26897  ang180lem3  27056  atanlogaddlem  27158  atanlogsublem  27160  atantan  27168  atans2  27176  cxploglim2  27223  emcllem6  27245  emcllem7  27246  lgamgulmlem2  27274  ftalem1  27317  ftalem2  27318  ppinncl  27418  chtrpcl  27419  vmalelog  27449  chtub  27456  logfacubnd  27465  logfacbnd3  27467  logfacrlim  27468  logexprlim  27469  mersenne  27471  perfectlem2  27474  bpos1lem  27526  bposlem1  27528  bposlem2  27529  bposlem3  27530  bposlem4  27531  bposlem5  27532  bposlem6  27533  lgseisen  27623  lgsquadlem1  27624  chebbnd1lem1  27713  chebbnd1lem3  27715  rpvmasumlem  27731  dchrvmasumlem2  27742  dchrvmasumlema  27744  dchrvmasumiflem1  27745  dchrisum0flblem2  27753  dchrisum0fno1  27755  dchrisum0re  27757  dirith2  27772  logdivsum  27777  mulog2sumlem1  27778  mulog2sumlem2  27779  log2sumbnd  27788  chpdifbndlem1  27797  chpdifbndlem2  27798  logdivbnd  27800  selberg3lem1  27801  pntpbnd1a  27829  pntpbnd2  27831  pntibndlem3  27836  pntlemn  27844  pntlemj  27847  pntlemk  27850  pnt  27858  addsgt0d  28287  ltmulnegs1d  28449  absmuls  28517  abssge0  28518  leabss  28521  nnsge1  28616  bdayfinbndlem1  28740  tgldimor  28852  axlowdim  29426  minvecolem4  31369  abrexctf  33196  nndiffz1  33265  wrdt2ind  33403  xrge0addgt0  33465  elrgspnlem2  33691  ply1coedeg  34007  drngdimgt0  34136  extdgfialglem2  34211  cos9thpiminplylem1  34300  esumcvg2  34605  inelcarsg  34830  carsgclctunlem2  34838  signsply0  35067  signsvtn  35100  erdsze2lem2  35791  lcmineqlem23  42925  lcmineqlem  42926  aks4d1p1p6  42947  aks4d1p1  42950  aks5lem2  43061  flt4lem7  43513  pellqrex  43728  reglogltb  43740  reglogleb  43741  rmspecnonsq  43756  rmspecpos  43765  areaquad  44065  hashnzfz2  45153  binomcxplemdvbinom  45185  binomcxplemnotnn0  45188  fmul01  46418  climconstmpt  46494  stoweidlem26  46862  stoweidlem44  46880  stoweidlem45  46881  wallispilem3  46903  wallispi  46906  stirlinglem11  46920  dirkertrigeqlem1  46934  dirkertrigeqlem3  46936  fourierdlem80  47022  fourierdlem102  47044  fourierdlem107  47049  fourierdlem114  47056  etransclem46  47116  fmtnoge3  48441  fmtno4prmfac  48483  perfectALTVlem2  48646  gboge9  48688  mogoldbb  48709  tgoldbach  48741  gpg3kgrtriexlem3  49009  gpg3kgrtriexlem6  49012  nnolog2flm1  49528