Theorem breqtrdi 5187

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-sn 4627  df-pr 4629  df-op 4633  df-br 5147

This theorem is referenced by:  breqtrrdi  5188  difsnen  9048  marypha1lem  9423  en2eleq  9998  en2other2  9999  dju0en  10165  pwdju1  10180  pwdjudom  10206  ackbij1lem5  10214  alephadd  10567  prlem934  11023  ltexprlem2  11027  recgt0ii  12115  discr  14198  faclbnd4lem1  14248  hashfun  14392  01sqrexlem7  15190  resqrex  15192  abs3lemi  15352  supcvg  15797  ege2le3  16028  cos01gt0  16129  sin02gt0  16130  bitsfzolem  16370  bitsmod  16372  prmreclem2  16845  f1otrspeq  19307  pmtrf  19315  pmtrmvd  19316  pmtrfinv  19321  efgi0  19580  efgi1  19581  dprdf1  19894  metustexhalf  24046  nlmvscnlem2  24183  icccmplem2  24320  xrge0tsms  24331  iimulcl  24434  pcoass  24521  ipcnlem2  24742  ivthlem3  24951  vitalilem4  25109  vitali  25111  dvef  25478  ply1rem  25662  aaliou3lem2  25837  abelthlem8  25932  abelthlem9  25933  cosne0  26019  sinord  26024  tanregt0  26029  argimgt0  26101  logf1o2  26139  logtayllem  26148  cxpcn3lem  26234  ang180lem2  26294  ang180lem3  26295  atanlogsublem  26399  bndatandm  26413  leibpi  26426  emcllem6  26484  emcllem7  26485  lgamgulmlem5  26516  lgamcvg2  26538  ftalem5  26560  basellem7  26570  basellem9  26572  ppieq0  26659  ppiub  26686  chpeq0  26690  chpub  26702  logfacrlim  26706  logexprlim  26707  bposlem1  26766  bposlem2  26767  lgslem3  26781  lgsquadlem1  26862  lgsquadlem3  26864  chebbnd1lem3  26953  chtppilim  26957  chpchtlim  26961  dchrvmasumiflem1  26983  dchrisum0re  26995  mudivsum  27012  mulog2sumlem2  27017  pntibndlem2  27073  pntlemb  27079  pntlemh  27081  ostth3  27120  crctcshwlkn0  29054  norm3lem  30379  nmopadjlem  31319  nmopcoadji  31331  hstle  31460  stadd3i  31478  strlem5  31485  pfxlsw2ccat  32093  gsumle  32219  locfinreflem  32757  xrge0iifcnv  32850  carsggect  33254  omsmeas  33259  signsply0  33499  signsvtp  33531  tgoldbachgtd  33611  sinccvglem  34594  faclim2  34655  poimirlem28  36453  ismblfin  36466  aks4d1p1p5  40877  sn-0lt1  41278  sn-inelr  41281  dffltz  41319  irrapxlem2  41493  pellexlem2  41500  areaquad  41897  dvgrat  43003  binomcxplemrat  43041  fmul01  44230  clim1fr1  44251  sinaover2ne0  44518  stoweidlem14  44664  stoweidlem16  44666  stoweidlem26  44676  stoweidlem41  44691  stoweidlem42  44692  stoweidlem45  44695  wallispi  44720  stirlinglem1  44724  stirlinglem12  44735  fourierdlem24  44781  fourierdlem107  44863  fouriersw  44881  meaiunincf  45133  meaiuninc3  45135  lincfsuppcl  46995  lincresunit3lem2  47062  lincresunit3  47063