Theorem breqtrdi 5111

Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)

Hypotheses

Ref	Expression
breqtrdi.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrdi.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
breqtrdi	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrdi

Step	Hyp	Ref	Expression
1		breqtrdi.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		eqid 2738	. 2 ⊢ 𝐴 = 𝐴
3		breqtrdi.2	. 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:  breqtrrdi  5112  difsnen  8794  marypha1lem  9122  en2eleq  9695  en2other2  9696  dju0en  9862  pwdju1  9877  pwdjudom  9903  ackbij1lem5  9911  alephadd  10264  prlem934  10720  ltexprlem2  10724  recgt0ii  11811  discr  13883  faclbnd4lem1  13935  hashfun  14080  sqrlem7  14888  resqrex  14890  abs3lemi  15050  supcvg  15496  ege2le3  15727  cos01gt0  15828  sin02gt0  15829  bitsfzolem  16069  bitsmod  16071  prmreclem2  16546  f1otrspeq  18970  pmtrf  18978  pmtrmvd  18979  pmtrfinv  18984  efgi0  19241  efgi1  19242  dprdf1  19551  metustexhalf  23618  nlmvscnlem2  23755  icccmplem2  23892  xrge0tsms  23903  iimulcl  24006  pcoass  24093  ipcnlem2  24313  ivthlem3  24522  vitalilem4  24680  vitali  24682  dvef  25049  ply1rem  25233  aaliou3lem2  25408  abelthlem8  25503  abelthlem9  25504  cosne0  25590  sinord  25595  tanregt0  25600  argimgt0  25672  logf1o2  25710  logtayllem  25719  cxpcn3lem  25805  ang180lem2  25865  ang180lem3  25866  atanlogsublem  25970  bndatandm  25984  leibpi  25997  emcllem6  26055  emcllem7  26056  lgamgulmlem5  26087  lgamcvg2  26109  ftalem5  26131  basellem7  26141  basellem9  26143  ppieq0  26230  ppiub  26257  chpeq0  26261  chpub  26273  logfacrlim  26277  logexprlim  26278  bposlem1  26337  bposlem2  26338  lgslem3  26352  lgsquadlem1  26433  lgsquadlem3  26435  chebbnd1lem3  26524  chtppilim  26528  chpchtlim  26532  dchrvmasumiflem1  26554  dchrisum0re  26566  mudivsum  26583  mulog2sumlem2  26588  pntibndlem2  26644  pntlemb  26650  pntlemh  26652  ostth3  26691  crctcshwlkn0  28087  norm3lem  29412  nmopadjlem  30352  nmopcoadji  30364  hstle  30493  stadd3i  30511  strlem5  30518  pfxlsw2ccat  31126  gsumle  31252  locfinreflem  31692  xrge0iifcnv  31785  carsggect  32185  omsmeas  32190  signsply0  32430  signsvtp  32462  tgoldbachgtd  32542  sinccvglem  33530  faclim2  33620  poimirlem28  35732  ismblfin  35745  aks4d1p1p5  40011  sn-0lt1  40353  sn-inelr  40356  dffltz  40387  irrapxlem2  40561  pellexlem2  40568  areaquad  40963  dvgrat  41819  binomcxplemrat  41857  fmul01  43011  clim1fr1  43032  sinaover2ne0  43299  stoweidlem14  43445  stoweidlem16  43447  stoweidlem26  43457  stoweidlem41  43472  stoweidlem42  43473  stoweidlem45  43476  wallispi  43501  stirlinglem1  43505  stirlinglem12  43516  fourierdlem24  43562  fourierdlem107  43644  fouriersw  43662  meaiunincf  43911  meaiuninc3  43913  lincfsuppcl  45642  lincresunit3lem2  45709  lincresunit3  45710