Theorem breqtrdi 5140

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  breqtrrdi  5141  difsnen  8991  marypha1lem  9340  en2eleq  9922  en2other2  9923  dju0en  10090  pwdju1  10105  pwdjudom  10129  ackbij1lem5  10137  alephadd  10492  prlem934  10948  ltexprlem2  10952  recgt0ii  12052  discr  14167  faclbnd4lem1  14220  hashfun  14364  01sqrexlem7  15175  resqrex  15177  abs3lemi  15338  supcvg  15783  ege2le3  16017  cos01gt0  16120  sin02gt0  16121  bitsfzolem  16365  bitsmod  16367  prmreclem2  16849  f1otrspeq  19380  pmtrf  19388  pmtrmvd  19389  pmtrfinv  19394  efgi0  19653  efgi1  19654  dprdf1  19968  gsumle  20078  metustexhalf  24504  nlmvscnlem2  24633  icccmplem2  24772  xrge0tsms  24783  iimulcl  24893  pcoass  24984  ipcnlem2  25204  ivthlem3  25414  vitalilem4  25572  vitali  25574  dvef  25944  ply1rem  26131  aaliou3lem2  26311  abelthlem8  26409  abelthlem9  26410  cosne0  26498  sinord  26503  tanregt0  26508  argimgt0  26581  logf1o2  26619  logtayllem  26628  cxpcn3lem  26717  ang180lem2  26780  ang180lem3  26781  atanlogsublem  26885  bndatandm  26899  leibpi  26912  emcllem6  26971  emcllem7  26972  lgamgulmlem5  27003  lgamcvg2  27025  ftalem5  27047  basellem7  27057  basellem9  27059  ppieq0  27146  ppiub  27175  chpeq0  27179  chpub  27191  logfacrlim  27195  logexprlim  27196  bposlem1  27255  bposlem2  27256  lgslem3  27270  lgsquadlem1  27351  lgsquadlem3  27353  chebbnd1lem3  27442  chtppilim  27446  chpchtlim  27450  dchrvmasumiflem1  27472  dchrisum0re  27484  mudivsum  27501  mulog2sumlem2  27506  pntibndlem2  27562  pntlemb  27568  pntlemh  27570  ostth3  27609  twocut  28423  addhalfcut  28459  recut  28494  crctcshwlkn0  29898  norm3lem  31228  nmopadjlem  32168  nmopcoadji  32180  hstle  32309  stadd3i  32327  strlem5  32334  pfxlsw2ccat  33034  elrgspnlem1  33326  vietadeg1  33736  locfinreflem  33999  xrge0iifcnv  34092  carsggect  34477  omsmeas  34482  signsply0  34710  signsvtp  34742  tgoldbachgtd  34821  sinccvglem  35868  faclim2  35944  poimirlem28  37851  ismblfin  37864  aks4d1p1p5  42397  sn-0lt1  42797  dffltz  42944  irrapxlem2  43132  pellexlem2  43139  areaquad  43525  dvgrat  44620  binomcxplemrat  44658  fmul01  45893  clim1fr1  45914  sinaover2ne0  46179  stoweidlem14  46325  stoweidlem16  46327  stoweidlem26  46337  stoweidlem41  46352  stoweidlem42  46353  stoweidlem45  46356  wallispi  46381  stirlinglem1  46385  stirlinglem12  46396  fourierdlem24  46442  fourierdlem107  46524  fouriersw  46542  meaiunincf  46794  meaiuninc3  46796  lincfsuppcl  48726  lincresunit3lem2  48793  lincresunit3  48794