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  28402  addhalfcut  28438  recut  28473  crctcshwlkn0  29877  norm3lem  31207  nmopadjlem  32147  nmopcoadji  32159  hstle  32288  stadd3i  32306  strlem5  32313  pfxlsw2ccat  33013  elrgspnlem1  33305  vietadeg1  33715  locfinreflem  33978  xrge0iifcnv  34071  carsggect  34456  omsmeas  34461  signsply0  34689  signsvtp  34721  tgoldbachgtd  34800  sinccvglem  35847  faclim2  35923  poimirlem28  37820  ismblfin  37833  aks4d1p1p5  42366  sn-0lt1  42766  dffltz  42913  irrapxlem2  43101  pellexlem2  43108  areaquad  43494  dvgrat  44589  binomcxplemrat  44627  fmul01  45862  clim1fr1  45883  sinaover2ne0  46148  stoweidlem14  46294  stoweidlem16  46296  stoweidlem26  46306  stoweidlem41  46321  stoweidlem42  46322  stoweidlem45  46325  wallispi  46350  stirlinglem1  46354  stirlinglem12  46365  fourierdlem24  46411  fourierdlem107  46493  fouriersw  46511  meaiunincf  46763  meaiuninc3  46765  lincfsuppcl  48695  lincresunit3lem2  48762  lincresunit3  48763