Theorem breqtrdi 5189

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5148

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  breqtrrdi  5190  difsnen  9052  marypha1lem  9427  en2eleq  10002  en2other2  10003  dju0en  10169  pwdju1  10184  pwdjudom  10210  ackbij1lem5  10218  alephadd  10571  prlem934  11027  ltexprlem2  11031  recgt0ii  12119  discr  14202  faclbnd4lem1  14252  hashfun  14396  01sqrexlem7  15194  resqrex  15196  abs3lemi  15356  supcvg  15801  ege2le3  16032  cos01gt0  16133  sin02gt0  16134  bitsfzolem  16374  bitsmod  16376  prmreclem2  16849  f1otrspeq  19314  pmtrf  19322  pmtrmvd  19323  pmtrfinv  19328  efgi0  19587  efgi1  19588  dprdf1  19902  metustexhalf  24064  nlmvscnlem2  24201  icccmplem2  24338  xrge0tsms  24349  iimulcl  24452  pcoass  24539  ipcnlem2  24760  ivthlem3  24969  vitalilem4  25127  vitali  25129  dvef  25496  ply1rem  25680  aaliou3lem2  25855  abelthlem8  25950  abelthlem9  25951  cosne0  26037  sinord  26042  tanregt0  26047  argimgt0  26119  logf1o2  26157  logtayllem  26166  cxpcn3lem  26252  ang180lem2  26312  ang180lem3  26313  atanlogsublem  26417  bndatandm  26431  leibpi  26444  emcllem6  26502  emcllem7  26503  lgamgulmlem5  26534  lgamcvg2  26556  ftalem5  26578  basellem7  26588  basellem9  26590  ppieq0  26677  ppiub  26704  chpeq0  26708  chpub  26720  logfacrlim  26724  logexprlim  26725  bposlem1  26784  bposlem2  26785  lgslem3  26799  lgsquadlem1  26880  lgsquadlem3  26882  chebbnd1lem3  26971  chtppilim  26975  chpchtlim  26979  dchrvmasumiflem1  27001  dchrisum0re  27013  mudivsum  27030  mulog2sumlem2  27035  pntibndlem2  27091  pntlemb  27097  pntlemh  27099  ostth3  27138  crctcshwlkn0  29072  norm3lem  30397  nmopadjlem  31337  nmopcoadji  31349  hstle  31478  stadd3i  31496  strlem5  31503  pfxlsw2ccat  32111  gsumle  32237  locfinreflem  32815  xrge0iifcnv  32908  carsggect  33312  omsmeas  33317  signsply0  33557  signsvtp  33589  tgoldbachgtd  33669  sinccvglem  34652  faclim2  34713  poimirlem28  36511  ismblfin  36524  aks4d1p1p5  40935  sn-0lt1  41336  sn-inelr  41339  dffltz  41377  irrapxlem2  41551  pellexlem2  41558  areaquad  41955  dvgrat  43061  binomcxplemrat  43099  fmul01  44286  clim1fr1  44307  sinaover2ne0  44574  stoweidlem14  44720  stoweidlem16  44722  stoweidlem26  44732  stoweidlem41  44747  stoweidlem42  44748  stoweidlem45  44751  wallispi  44776  stirlinglem1  44780  stirlinglem12  44791  fourierdlem24  44837  fourierdlem107  44919  fouriersw  44937  meaiunincf  45189  meaiuninc3  45191  lincfsuppcl  47084  lincresunit3lem2  47151  lincresunit3  47152