Theorem breqtrdi 5151

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is used by:  breqtrrdi  5152  difsnen  9045  marypha1lem  9391  en2eleq  9999  en2other2  10000  dju0en  10166  pwdju1  10181  pwdjudom  10205  ackbij1lem5  10213  alephadd  10568  prlem934  11024  ltexprlem2  11028  recgt0ii  12127  discr  14283  faclbnd4lem1  14336  hashfun  14481  01sqrexlem7  15306  resqrex  15308  abs3lemi  15469  supcvg  15917  ege2le3  16150  cos01gt0  16253  sin02gt0  16254  bitsfzolem  16498  bitsmod  16500  prmreclem2  16983  f1otrspeq  19523  pmtrf  19531  pmtrmvd  19532  pmtrfinv  19537  efgi0  19796  efgi1  19797  dprdf1  20111  gsumle  20221  metustexhalf  24724  nlmvscnlem2  24853  icccmplem2  24992  xrge0tsms  25003  iimulcl  25107  pcoass  25194  ipcnlem2  25414  ivthlem3  25623  vitalilem4  25781  vitali  25783  dvef  26150  ply1rem  26334  aaliou3lem2  26517  abelthlem8  26613  abelthlem9  26614  cosne0  26705  sinord  26710  tanregt0  26715  argimgt0  26788  logf1o2  26826  logtayllem  26835  cxpcn3lem  26923  ang180lem2  26986  ang180lem3  26987  atanlogsublem  27091  bndatandm  27105  leibpi  27118  emcllem6  27176  emcllem7  27177  lgamgulmlem5  27208  lgamcvg2  27230  ftalem5  27252  basellem7  27262  basellem9  27264  ppieq0  27351  ppiub  27379  chpeq0  27383  chpub  27395  logfacrlim  27399  logexprlim  27400  bposlem1  27459  bposlem2  27460  lgslem3  27474  lgsquadlem1  27555  lgsquadlem3  27557  chebbnd1lem3  27646  chtppilim  27650  chpchtlim  27654  dchrvmasumiflem1  27676  dchrisum0re  27688  mudivsum  27705  mulog2sumlem2  27710  pntibndlem2  27766  pntlemb  27772  pntlemh  27774  ostth3  27813  twocut  28627  addhalfcut  28663  recut  28698  crctcshwlkn0  30181  norm3lem  31512  nmopadjlem  32452  nmopcoadji  32464  hstle  32593  stadd3i  32611  strlem5  32618  pfxlsw2ccat  33279  elrgspnlem1  33571  vietadeg1  33977  locfinreflem  34239  xrge0iifcnv  34332  carsggect  34717  omsmeas  34722  signsply0  34947  signsvtp  34979  tgoldbachgtd  35058  1enumen  35494  sinccvglem  36172  faclim2  36248  poimirlem28  38327  ismblfin  38340  aks4d1p1p5  42870  sn-0lt1  43277  dffltz  43394  irrapxlem2  43578  pellexlem2  43585  areaquad  43971  dvgrat  45050  binomcxplemrat  45088  fmul01  46324  clim1fr1  46345  sinaover2ne0  46610  stoweidlem14  46756  stoweidlem16  46758  stoweidlem26  46768  stoweidlem41  46783  stoweidlem42  46784  stoweidlem45  46787  wallispi  46812  stirlinglem1  46816  stirlinglem12  46827  fourierdlem24  46873  fourierdlem107  46955  fouriersw  46973  meaiunincf  47225  meaiuninc3  47227  lincfsuppcl  49221  lincresunit3lem2  49288  lincresunit3  49289