Theorem breqtrdi 5154

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112

This theorem is referenced by:  breqtrrdi  5155  difsnen  9047  marypha1lem  9393  en2eleq  9992  en2other2  9993  dju0en  10159  pwdju1  10174  pwdjudom  10198  ackbij1lem5  10206  alephadd  10562  prlem934  11018  ltexprlem2  11022  recgt0ii  12121  discr  14276  faclbnd4lem1  14329  hashfun  14474  01sqrexlem7  15299  resqrex  15301  abs3lemi  15462  supcvg  15910  ege2le3  16144  cos01gt0  16247  sin02gt0  16248  bitsfzolem  16492  bitsmod  16494  prmreclem2  16977  f1otrspeq  19517  pmtrf  19525  pmtrmvd  19526  pmtrfinv  19531  efgi0  19790  efgi1  19791  dprdf1  20105  gsumle  20215  metustexhalf  24682  nlmvscnlem2  24811  icccmplem2  24950  xrge0tsms  24961  iimulcl  25065  pcoass  25152  ipcnlem2  25372  ivthlem3  25581  vitalilem4  25739  vitali  25741  dvef  26108  ply1rem  26292  aaliou3lem2  26473  abelthlem8  26568  abelthlem9  26569  cosne0  26660  sinord  26665  tanregt0  26670  argimgt0  26743  logf1o2  26781  logtayllem  26790  cxpcn3lem  26878  ang180lem2  26941  ang180lem3  26942  atanlogsublem  27046  bndatandm  27060  leibpi  27073  emcllem6  27131  emcllem7  27132  lgamgulmlem5  27163  lgamcvg2  27185  ftalem5  27207  basellem7  27217  basellem9  27219  ppieq0  27306  ppiub  27334  chpeq0  27338  chpub  27350  logfacrlim  27354  logexprlim  27355  bposlem1  27414  bposlem2  27415  lgslem3  27429  lgsquadlem1  27510  lgsquadlem3  27512  chebbnd1lem3  27601  chtppilim  27605  chpchtlim  27609  dchrvmasumiflem1  27631  dchrisum0re  27643  mudivsum  27660  mulog2sumlem2  27665  pntibndlem2  27721  pntlemb  27727  pntlemh  27729  ostth3  27768  twocut  28582  addhalfcut  28618  recut  28653  crctcshwlkn0  30111  norm3lem  31442  nmopadjlem  32382  nmopcoadji  32394  hstle  32523  stadd3i  32541  strlem5  32548  pfxlsw2ccat  33211  elrgspnlem1  33503  vietadeg1  33913  locfinreflem  34175  xrge0iifcnv  34268  carsggect  34653  omsmeas  34658  signsply0  34883  signsvtp  34915  tgoldbachgtd  34994  1enumen  35428  sinccvglem  36097  faclim2  36173  poimirlem28  38222  ismblfin  38235  aks4d1p1p5  42767  sn-0lt1  43174  dffltz  43293  irrapxlem2  43477  pellexlem2  43484  areaquad  43870  dvgrat  44949  binomcxplemrat  44987  fmul01  46223  clim1fr1  46244  sinaover2ne0  46509  stoweidlem14  46655  stoweidlem16  46657  stoweidlem26  46667  stoweidlem41  46682  stoweidlem42  46683  stoweidlem45  46686  wallispi  46711  stirlinglem1  46715  stirlinglem12  46726  fourierdlem24  46772  fourierdlem107  46854  fouriersw  46872  meaiunincf  47124  meaiuninc3  47126  lincfsuppcl  49113  lincresunit3lem2  49180  lincresunit3  49181