Theorem breqtrdi 5133

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  breqtrrdi  5134  difsnen  8976  marypha1lem  9323  en2eleq  9902  en2other2  9903  dju0en  10070  pwdju1  10085  pwdjudom  10109  ackbij1lem5  10117  alephadd  10471  prlem934  10927  ltexprlem2  10931  recgt0ii  12031  discr  14147  faclbnd4lem1  14200  hashfun  14344  01sqrexlem7  15155  resqrex  15157  abs3lemi  15318  supcvg  15763  ege2le3  15997  cos01gt0  16100  sin02gt0  16101  bitsfzolem  16345  bitsmod  16347  prmreclem2  16829  f1otrspeq  19326  pmtrf  19334  pmtrmvd  19335  pmtrfinv  19340  efgi0  19599  efgi1  19600  dprdf1  19914  gsumle  20024  metustexhalf  24442  nlmvscnlem2  24571  icccmplem2  24710  xrge0tsms  24721  iimulcl  24831  pcoass  24922  ipcnlem2  25142  ivthlem3  25352  vitalilem4  25510  vitali  25512  dvef  25882  ply1rem  26069  aaliou3lem2  26249  abelthlem8  26347  abelthlem9  26348  cosne0  26436  sinord  26441  tanregt0  26446  argimgt0  26519  logf1o2  26557  logtayllem  26566  cxpcn3lem  26655  ang180lem2  26718  ang180lem3  26719  atanlogsublem  26823  bndatandm  26837  leibpi  26850  emcllem6  26909  emcllem7  26910  lgamgulmlem5  26941  lgamcvg2  26963  ftalem5  26985  basellem7  26995  basellem9  26997  ppieq0  27084  ppiub  27113  chpeq0  27117  chpub  27129  logfacrlim  27133  logexprlim  27134  bposlem1  27193  bposlem2  27194  lgslem3  27208  lgsquadlem1  27289  lgsquadlem3  27291  chebbnd1lem3  27380  chtppilim  27384  chpchtlim  27388  dchrvmasumiflem1  27410  dchrisum0re  27422  mudivsum  27439  mulog2sumlem2  27444  pntibndlem2  27500  pntlemb  27506  pntlemh  27508  ostth3  27547  twocut  28317  addhalfcut  28350  recut  28369  crctcshwlkn0  29770  norm3lem  31097  nmopadjlem  32037  nmopcoadji  32049  hstle  32178  stadd3i  32196  strlem5  32203  pfxlsw2ccat  32901  elrgspnlem1  33191  locfinreflem  33823  xrge0iifcnv  33916  carsggect  34302  omsmeas  34307  signsply0  34535  signsvtp  34567  tgoldbachgtd  34646  sinccvglem  35665  faclim2  35741  poimirlem28  37648  ismblfin  37661  aks4d1p1p5  42068  sn-0lt1  42468  dffltz  42627  irrapxlem2  42816  pellexlem2  42823  areaquad  43209  dvgrat  44305  binomcxplemrat  44343  fmul01  45581  clim1fr1  45602  sinaover2ne0  45869  stoweidlem14  46015  stoweidlem16  46017  stoweidlem26  46027  stoweidlem41  46042  stoweidlem42  46043  stoweidlem45  46046  wallispi  46071  stirlinglem1  46075  stirlinglem12  46086  fourierdlem24  46132  fourierdlem107  46214  fouriersw  46232  meaiunincf  46484  meaiuninc3  46486  lincfsuppcl  48418  lincresunit3lem2  48485  lincresunit3  48486