Theorem breqtrdi 5145

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  breqtrrdi  5146  difsnen  9078  marypha1lem  9425  en2eleq  10087  en2other2  10088  dju0en  10254  pwdju1  10269  pwdjudom  10293  ackbij1lem5  10301  alephadd  10662  prlem934  11118  ltexprlem2  11122  recgt0ii  12223  discr  14384  faclbnd4lem1  14437  hashfun  14582  01sqrexlem7  15415  resqrex  15417  abs3lemi  15578  supcvg  16025  ege2le3  16256  cos01gt0  16359  sin02gt0  16360  bitsfzolem  16604  bitsmod  16606  prmreclem2  17095  f1otrspeq  19661  pmtrf  19669  pmtrmvd  19670  pmtrfinv  19675  efgi0  19934  efgi1  19935  dprdf1  20249  gsumle  20359  metustexhalf  24875  nlmvscnlem2  25004  icccmplem2  25143  xrge0tsms  25154  iimulcl  25258  pcoass  25345  ipcnlem2  25565  ivthlem3  25774  vitalilem4  25932  vitali  25934  dvef  26300  ply1rem  26484  aaliou3lem2  26670  abelthlem8  26766  abelthlem9  26767  cosne0  26857  sinord  26862  tanregt0  26867  argimgt0  26940  logf1o2  26978  logtayllem  26987  cxpcn3lem  27075  ang180lem2  27138  ang180lem3  27139  atanlogsublem  27243  bndatandm  27257  leibpi  27270  emcllem6  27328  emcllem7  27329  lgamgulmlem5  27360  lgamcvg2  27382  ftalem5  27404  basellem7  27414  basellem9  27416  ppieq0  27503  ppiub  27531  chpeq0  27535  chpub  27547  logfacrlim  27551  logexprlim  27552  bposlem1  27611  bposlem2  27612  lgslem3  27626  lgsquadlem1  27707  lgsquadlem3  27709  chebbnd1lem3  27798  chtppilim  27802  chpchtlim  27806  dchrvmasumiflem1  27828  dchrisum0re  27840  mudivsum  27857  mulog2sumlem2  27862  pntibndlem2  27918  pntlemb  27924  pntlemh  27926  ostth3  27965  twocut  28809  addhalfcut  28845  recut  28880  crctcshwlkn0  30410  norm3lem  31751  nmopadjlem  32691  nmopcoadji  32703  hstle  32832  stadd3i  32850  strlem5  32857  pfxlsw2ccat  33513  elrgspnlem1  33803  vietadeg1  34210  locfinreflem  34472  xrge0iifcnv  34565  carsggect  34950  omsmeas  34955  signsply0  35180  signsvtp  35212  tgoldbachgtd  35291  1enumen  35723  sinccvglem  36437  faclim2  36513  poimirlem28  38567  ismblfin  38580  aks4d1p1p5  43126  sn-0lt1  43540  dffltz  43671  irrapxlem2  43830  pellexlem2  43837  areaquad  44218  dvgrat  45296  binomcxplemrat  45334  fmul01  46592  clim1fr1  46613  sinaover2ne0  46878  stoweidlem14  47024  stoweidlem16  47026  stoweidlem26  47036  stoweidlem41  47051  stoweidlem42  47052  stoweidlem45  47055  wallispi  47080  stirlinglem1  47084  stirlinglem12  47095  fourierdlem24  47141  fourierdlem107  47223  fouriersw  47241  meaiunincf  47493  meaiuninc3  47495  lincfsuppcl  49525  lincresunit3lem2  49592  lincresunit3  49593