Theorem eqbrtrrid 5102

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  enpr1g  8575  undom  8605  fidomdm  8801  prdom2  9432  infdju1  9615  infdif  9631  cfslb2n  9690  fin56  9815  dmct  9946  gchxpidm  10091  rankcf  10199  r1tskina  10204  tskuni  10205  ltsonq  10391  addgt0  11126  addgegt0  11127  addgtge0  11128  addge0  11129  expge1  13467  fsumrlim  15166  isumsup  15202  climcndslem1  15204  fprodge1  15349  3dvds  15680  bitsinv1lem  15790  phicl2  16105  frgpnabllem1  18993  lt6abl  19015  pgpfaclem2  19204  unitmulcl  19414  gsumply1eq  20473  xrsdsreclblem  20591  znidomb  20708  lindfres  20967  2ndcdisj2  22065  hmphindis  22405  tsms0  22750  tgptsmscls  22758  metustexhalf  23166  xrhmeo  23550  pcoass  23628  ovoliunlem1  24103  ismbl2  24128  voliunlem2  24152  ioombl1lem4  24162  itg2ge0  24336  itg2addlem  24359  itgge0  24411  dvfsumrlimge0  24627  abelthlem1  25019  abelthlem2  25020  pilem2  25040  rplogcl  25187  logge0  25188  argimgt0  25195  logdivlti  25203  logf1o2  25233  dvlog2lem  25235  ang180lem3  25389  atanlogaddlem  25491  atanlogsublem  25493  atantan  25501  atans2  25509  cxploglim2  25556  emcllem6  25578  emcllem7  25579  lgamgulmlem2  25607  ftalem1  25650  ftalem2  25651  ppinncl  25751  chtrpcl  25752  vmalelog  25781  chtub  25788  logfacubnd  25797  logfacbnd3  25799  logfacrlim  25800  logexprlim  25801  mersenne  25803  perfectlem2  25806  bpos1lem  25858  bposlem1  25860  bposlem2  25861  bposlem3  25862  bposlem4  25863  bposlem5  25864  bposlem6  25865  lgseisen  25955  lgsquadlem1  25956  chebbnd1lem1  26045  chebbnd1lem3  26047  rpvmasumlem  26063  dchrvmasumlem2  26074  dchrvmasumlema  26076  dchrvmasumiflem1  26077  dchrisum0flblem2  26085  dchrisum0fno1  26087  dchrisum0re  26089  dirith2  26104  logdivsum  26109  mulog2sumlem1  26110  mulog2sumlem2  26111  log2sumbnd  26120  chpdifbndlem1  26129  chpdifbndlem2  26130  logdivbnd  26132  selberg3lem1  26133  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem3  26168  pntlemn  26176  pntlemj  26179  pntlemk  26182  pnt  26190  tgldimor  26288  axlowdim  26747  minvecolem4  28657  abrexct  30452  abrexctf  30454  nndiffz1  30509  wrdt2ind  30627  xrge0addgt0  30678  drngdimgt0  31016  esumcvg2  31346  inelcarsg  31569  carsgclctunlem2  31577  signsply0  31821  signsvtn  31854  erdsze2lem2  32451  2xp3dxp2ge1d  39146  pellqrex  39525  reglogltb  39537  reglogleb  39538  rmspecnonsq  39553  rmspecpos  39562  areaquad  39872  hashnzfz2  40702  binomcxplemdvbinom  40734  binomcxplemnotnn0  40737  fmul01  41910  climconstmpt  41988  stoweidlem26  42360  stoweidlem44  42378  stoweidlem45  42379  wallispilem3  42401  wallispi  42404  stirlinglem11  42418  dirkertrigeqlem1  42432  dirkertrigeqlem3  42434  fourierdlem80  42520  fourierdlem102  42542  fourierdlem107  42547  fourierdlem114  42554  etransclem46  42614  fmtnoge3  43741  fmtno4prmfac  43783  perfectALTVlem2  43936  gboge9  43978  mogoldbb  43999  tgoldbach  44031  nnolog2flm1  44699