Theorem breqtrdi 5130

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  breqtrrdi  5131  difsnen  8972  marypha1lem  9317  en2eleq  9899  en2other2  9900  dju0en  10067  pwdju1  10082  pwdjudom  10106  ackbij1lem5  10114  alephadd  10468  prlem934  10924  ltexprlem2  10928  recgt0ii  12028  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  19359  pmtrf  19367  pmtrmvd  19368  pmtrfinv  19373  efgi0  19632  efgi1  19633  dprdf1  19947  gsumle  20057  metustexhalf  24471  nlmvscnlem2  24600  icccmplem2  24739  xrge0tsms  24750  iimulcl  24860  pcoass  24951  ipcnlem2  25171  ivthlem3  25381  vitalilem4  25539  vitali  25541  dvef  25911  ply1rem  26098  aaliou3lem2  26278  abelthlem8  26376  abelthlem9  26377  cosne0  26465  sinord  26470  tanregt0  26475  argimgt0  26548  logf1o2  26586  logtayllem  26595  cxpcn3lem  26684  ang180lem2  26747  ang180lem3  26748  atanlogsublem  26852  bndatandm  26866  leibpi  26879  emcllem6  26938  emcllem7  26939  lgamgulmlem5  26970  lgamcvg2  26992  ftalem5  27014  basellem7  27024  basellem9  27026  ppieq0  27113  ppiub  27142  chpeq0  27146  chpub  27158  logfacrlim  27162  logexprlim  27163  bposlem1  27222  bposlem2  27223  lgslem3  27237  lgsquadlem1  27318  lgsquadlem3  27320  chebbnd1lem3  27409  chtppilim  27413  chpchtlim  27417  dchrvmasumiflem1  27439  dchrisum0re  27451  mudivsum  27468  mulog2sumlem2  27473  pntibndlem2  27529  pntlemb  27535  pntlemh  27537  ostth3  27576  twocut  28346  addhalfcut  28379  recut  28398  crctcshwlkn0  29799  norm3lem  31129  nmopadjlem  32069  nmopcoadji  32081  hstle  32210  stadd3i  32228  strlem5  32235  pfxlsw2ccat  32931  elrgspnlem1  33209  locfinreflem  33853  xrge0iifcnv  33946  carsggect  34331  omsmeas  34336  signsply0  34564  signsvtp  34596  tgoldbachgtd  34675  sinccvglem  35716  faclim2  35792  poimirlem28  37687  ismblfin  37700  aks4d1p1p5  42167  sn-0lt1  42567  dffltz  42726  irrapxlem2  42915  pellexlem2  42922  areaquad  43308  dvgrat  44404  binomcxplemrat  44442  fmul01  45679  clim1fr1  45700  sinaover2ne0  45965  stoweidlem14  46111  stoweidlem16  46113  stoweidlem26  46123  stoweidlem41  46138  stoweidlem42  46139  stoweidlem45  46142  wallispi  46167  stirlinglem1  46171  stirlinglem12  46182  fourierdlem24  46228  fourierdlem107  46310  fouriersw  46328  meaiunincf  46580  meaiuninc3  46582  lincfsuppcl  48513  lincresunit3lem2  48580  lincresunit3  48581