Theorem breqtrdi 5126

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  breqtrrdi  5127  difsnen  8997  marypha1lem  9346  en2eleq  9930  en2other2  9931  dju0en  10098  pwdju1  10113  pwdjudom  10137  ackbij1lem5  10145  alephadd  10500  prlem934  10956  ltexprlem2  10960  recgt0ii  12062  discr  14202  faclbnd4lem1  14255  hashfun  14399  01sqrexlem7  15210  resqrex  15212  abs3lemi  15373  supcvg  15821  ege2le3  16055  cos01gt0  16158  sin02gt0  16159  bitsfzolem  16403  bitsmod  16405  prmreclem2  16888  f1otrspeq  19422  pmtrf  19430  pmtrmvd  19431  pmtrfinv  19436  efgi0  19695  efgi1  19696  dprdf1  20010  gsumle  20120  metustexhalf  24521  nlmvscnlem2  24650  icccmplem2  24789  xrge0tsms  24800  iimulcl  24904  pcoass  24991  ipcnlem2  25211  ivthlem3  25420  vitalilem4  25578  vitali  25580  dvef  25947  ply1rem  26131  aaliou3lem2  26309  abelthlem8  26404  abelthlem9  26405  cosne0  26493  sinord  26498  tanregt0  26503  argimgt0  26576  logf1o2  26614  logtayllem  26623  cxpcn3lem  26711  ang180lem2  26774  ang180lem3  26775  atanlogsublem  26879  bndatandm  26893  leibpi  26906  emcllem6  26964  emcllem7  26965  lgamgulmlem5  26996  lgamcvg2  27018  ftalem5  27040  basellem7  27050  basellem9  27052  ppieq0  27139  ppiub  27167  chpeq0  27171  chpub  27183  logfacrlim  27187  logexprlim  27188  bposlem1  27247  bposlem2  27248  lgslem3  27262  lgsquadlem1  27343  lgsquadlem3  27345  chebbnd1lem3  27434  chtppilim  27438  chpchtlim  27442  dchrvmasumiflem1  27464  dchrisum0re  27476  mudivsum  27493  mulog2sumlem2  27498  pntibndlem2  27554  pntlemb  27560  pntlemh  27562  ostth3  27601  twocut  28415  addhalfcut  28451  recut  28486  crctcshwlkn0  29889  norm3lem  31220  nmopadjlem  32160  nmopcoadji  32172  hstle  32301  stadd3i  32319  strlem5  32326  pfxlsw2ccat  33010  elrgspnlem1  33303  vietadeg1  33722  locfinreflem  33984  xrge0iifcnv  34077  carsggect  34462  omsmeas  34467  signsply0  34695  signsvtp  34727  tgoldbachgtd  34806  sinccvglem  35854  faclim2  35930  poimirlem28  37969  ismblfin  37982  aks4d1p1p5  42514  sn-0lt1  42920  dffltz  43067  irrapxlem2  43251  pellexlem2  43258  areaquad  43644  dvgrat  44739  binomcxplemrat  44777  fmul01  46010  clim1fr1  46031  sinaover2ne0  46296  stoweidlem14  46442  stoweidlem16  46444  stoweidlem26  46454  stoweidlem41  46469  stoweidlem42  46470  stoweidlem45  46473  wallispi  46498  stirlinglem1  46502  stirlinglem12  46513  fourierdlem24  46559  fourierdlem107  46641  fouriersw  46659  meaiunincf  46911  meaiuninc3  46913  lincfsuppcl  48889  lincresunit3lem2  48956  lincresunit3  48957