Theorem breqtrrdi 5155

Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
breqtrrdi.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
breqtrrdi	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrdi

Step	Hyp	Ref	Expression
1		breqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2778	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtrdi 5154	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:  enpr2d  9045  pw2eng  9071  undjudom  10151  dju1en  10155  djucomen  10161  djuassen  10162  xpdjuen  10163  infdjuabs  10188  ackbij1lem9  10210  unsnen  10537  1nqenq  10947  gtndiv  12673  xov1plusxeqvd  13525  intfrac2  13891  serle  14093  discr1  14275  faclbnd4lem1  14329  01sqrexlem1  15293  01sqrexlem4  15296  01sqrexlem7  15299  supcvg  15910  ege2le3  16144  eirrlem  16260  ruclem12  16297  bitsfzo  16493  pcprendvds  16900  pcpremul  16903  pcfaclem  16958  infpnlem2  16971  yonedainv  18337  srgbinomlem4  20311  lmcn2  23775  hmph0  23921  icccmplem2  24950  reconnlem2  24954  xrge0tsms  24961  minveclem2  25554  minveclem3b  25556  minveclem4  25560  minveclem6  25562  ivthlem2  25580  ivthlem3  25581  vitalilem2  25737  itg2seq  25870  itg2monolem1  25878  itg2monolem2  25879  itg2monolem3  25880  dveflem  26107  dvferm1lem  26112  dvferm2lem  26114  c1liplem1  26124  lhop1lem  26141  dvcvx  26148  plyeq0lem  26336  radcnvcl  26546  radcnvle  26549  psercnlem1  26554  psercn  26555  pilem3  26582  tangtx  26636  cos02pilt1  26657  cosne0  26660  recosf1o  26666  resinf1o  26667  efif1olem4  26676  logi  26718  logimul  26745  logcnlem3  26775  logf1o2  26781  ang180lem2  26941  heron  26969  acoscos  27024  emcllem7  27132  fsumharmonic  27142  ftalem2  27204  basellem1  27211  basellem2  27212  basellem3  27213  basellem5  27215  bposlem1  27414  bposlem2  27415  bposlem3  27416  lgsdirprm  27461  chebbnd1lem1  27599  chebbnd1lem2  27600  chebbnd1lem3  27601  mulog2sumlem2  27665  pntpbnd1a  27715  pntpbnd1  27716  pntpbnd2  27717  pntibndlem2  27721  pntlemc  27725  pntlemb  27727  pntlemg  27728  pntlemh  27729  pntlemr  27732  ostth2lem2  27764  ostth2lem3  27765  ostth2lem4  27766  ostth3  27768  axsegconlem3  29210  clwlkclwwlk2  30295  siilem1  31144  minvecolem2  31168  minvecolem4  31173  minvecolem5  31174  minvecolem6  31175  nmopcoi  32388  staddi  32539  cycpmco2lem4  33390  cycpmco2lem5  33391  iconstr  34101  hgt750lemd  34980  climlec3  36159  poimirlem26  38220  ftc1anclem8  38274  cntotbnd  38370  dalemply  40353  dalemsly  40354  dalem5  40366  dalem13  40375  dalem17  40379  dalem55  40426  dalem57  40428  lhpat3  40745  cdleme22aa  41038  aks4d1p1p7  42766  evlselv  43248  jm2.27c  43661  hashnzfz2  44958  supxrubd  45758  suprnmpt  45819  fzisoeu  45946  upbdrech  45951  recnnltrp  46019  uzublem  46071  fmul01  46223  limsupubuzlem  46353  limsupequzmptlem  46369  ioodvbdlimc1lem2  46573  ioodvbdlimc2lem  46575  stoweidlem36  46677  stoweidlem41  46682  wallispi2  46714  dirkercncflem1  46744  fourierdlem6  46754  fourierdlem7  46755  fourierdlem19  46767  fourierdlem20  46768  fourierdlem24  46772  fourierdlem25  46773  fourierdlem26  46774  fourierdlem30  46778  fourierdlem31  46779  fourierdlem42  46790  fourierdlem47  46794  fourierdlem48  46795  fourierdlem49  46796  fourierdlem63  46810  fourierdlem64  46811  fourierdlem65  46812  fourierdlem71  46818  fourierdlem79  46826  fourierdlem89  46836  fourierdlem90  46837  fourierdlem91  46838  fouriersw  46872  etransclem28  46903  etransclem48  46923  hoidmv1lelem1  47232  hoidmv1lelem3  47234  hoidmvlelem1  47236  hoidmvlelem4  47239  bgoldbtbndlem2  48495  gpg3kgrtriexlem4  48775  gpg3kgrtriexlem6  48777  lincresunit3lem2  49180  lincresunit3  49181  resum2sqgt0  49407  amgmwlem  50511