Theorem breqtrdi 5138

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

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

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  breqtrrdi  5139  difsnen  8989  marypha1lem  9338  en2eleq  9920  en2other2  9921  dju0en  10088  pwdju1  10103  pwdjudom  10127  ackbij1lem5  10135  alephadd  10490  prlem934  10946  ltexprlem2  10950  recgt0ii  12050  discr  14165  faclbnd4lem1  14218  hashfun  14362  01sqrexlem7  15173  resqrex  15175  abs3lemi  15336  supcvg  15781  ege2le3  16015  cos01gt0  16118  sin02gt0  16119  bitsfzolem  16363  bitsmod  16365  prmreclem2  16847  f1otrspeq  19378  pmtrf  19386  pmtrmvd  19387  pmtrfinv  19392  efgi0  19651  efgi1  19652  dprdf1  19966  gsumle  20076  metustexhalf  24502  nlmvscnlem2  24631  icccmplem2  24770  xrge0tsms  24781  iimulcl  24891  pcoass  24982  ipcnlem2  25202  ivthlem3  25412  vitalilem4  25570  vitali  25572  dvef  25942  ply1rem  26129  aaliou3lem2  26309  abelthlem8  26407  abelthlem9  26408  cosne0  26496  sinord  26501  tanregt0  26506  argimgt0  26579  logf1o2  26617  logtayllem  26626  cxpcn3lem  26715  ang180lem2  26778  ang180lem3  26779  atanlogsublem  26883  bndatandm  26897  leibpi  26910  emcllem6  26969  emcllem7  26970  lgamgulmlem5  27001  lgamcvg2  27023  ftalem5  27045  basellem7  27055  basellem9  27057  ppieq0  27144  ppiub  27173  chpeq0  27177  chpub  27189  logfacrlim  27193  logexprlim  27194  bposlem1  27253  bposlem2  27254  lgslem3  27268  lgsquadlem1  27349  lgsquadlem3  27351  chebbnd1lem3  27440  chtppilim  27444  chpchtlim  27448  dchrvmasumiflem1  27470  dchrisum0re  27482  mudivsum  27499  mulog2sumlem2  27504  pntibndlem2  27560  pntlemb  27566  pntlemh  27568  ostth3  27607  twocut  28400  addhalfcut  28436  recut  28471  crctcshwlkn0  29875  norm3lem  31205  nmopadjlem  32145  nmopcoadji  32157  hstle  32286  stadd3i  32304  strlem5  32311  pfxlsw2ccat  33011  elrgspnlem1  33303  vietadeg1  33713  locfinreflem  33976  xrge0iifcnv  34069  carsggect  34454  omsmeas  34459  signsply0  34687  signsvtp  34719  tgoldbachgtd  34798  sinccvglem  35845  faclim2  35921  poimirlem28  37818  ismblfin  37831  aks4d1p1p5  42364  sn-0lt1  42767  dffltz  42914  irrapxlem2  43102  pellexlem2  43109  areaquad  43495  dvgrat  44590  binomcxplemrat  44628  fmul01  45863  clim1fr1  45884  sinaover2ne0  46149  stoweidlem14  46295  stoweidlem16  46297  stoweidlem26  46307  stoweidlem41  46322  stoweidlem42  46323  stoweidlem45  46326  wallispi  46351  stirlinglem1  46355  stirlinglem12  46366  fourierdlem24  46412  fourierdlem107  46494  fouriersw  46512  meaiunincf  46764  meaiuninc3  46766  lincfsuppcl  48696  lincresunit3lem2  48763  lincresunit3  48764