Theorem breqtrrdi 5139

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

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

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 2707

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 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  enpr2d  8987  pw2eng  9013  undjudom  10080  dju1en  10084  djucomen  10090  djuassen  10091  xpdjuen  10092  infdjuabs  10117  ackbij1lem9  10139  unsnen  10465  1nqenq  10875  gtndiv  12571  xov1plusxeqvd  13416  intfrac2  13780  serle  13982  discr1  14164  faclbnd4lem1  14218  01sqrexlem1  15167  01sqrexlem4  15170  01sqrexlem7  15173  supcvg  15781  ege2le3  16015  eirrlem  16131  ruclem12  16168  bitsfzo  16364  pcprendvds  16770  pcpremul  16773  pcfaclem  16828  infpnlem2  16841  yonedainv  18206  srgbinomlem4  20166  lmcn2  23595  hmph0  23741  icccmplem2  24770  reconnlem2  24774  xrge0tsms  24781  minveclem2  25384  minveclem3b  25386  minveclem4  25390  minveclem6  25392  ivthlem2  25411  ivthlem3  25412  vitalilem2  25568  itg2seq  25701  itg2monolem1  25709  itg2monolem2  25710  itg2monolem3  25711  dveflem  25941  dvferm1lem  25946  dvferm2lem  25948  c1liplem1  25959  lhop1lem  25976  dvcvx  25983  plyeq0lem  26173  radcnvcl  26384  radcnvle  26387  psercnlem1  26393  psercn  26394  pilem3  26421  tangtx  26472  cos02pilt1  26493  cosne0  26496  recosf1o  26502  resinf1o  26503  efif1olem4  26512  logi  26554  logimul  26581  logcnlem3  26611  logf1o2  26617  ang180lem2  26778  heron  26806  acoscos  26861  emcllem7  26970  fsumharmonic  26980  ftalem2  27042  basellem1  27049  basellem2  27050  basellem3  27051  basellem5  27053  bposlem1  27253  bposlem2  27254  bposlem3  27255  lgsdirprm  27300  chebbnd1lem1  27438  chebbnd1lem2  27439  chebbnd1lem3  27440  mulog2sumlem2  27504  pntpbnd1a  27554  pntpbnd1  27555  pntpbnd2  27556  pntibndlem2  27560  pntlemc  27564  pntlemb  27566  pntlemg  27567  pntlemh  27568  pntlemr  27571  ostth2lem2  27603  ostth2lem3  27604  ostth2lem4  27605  ostth3  27607  axsegconlem3  28973  clwlkclwwlk2  30059  siilem1  30907  minvecolem2  30931  minvecolem4  30936  minvecolem5  30937  minvecolem6  30938  nmopcoi  32151  staddi  32302  cycpmco2lem4  33190  cycpmco2lem5  33191  iconstr  33902  hgt750lemd  34784  climlec3  35907  poimirlem26  37816  ftc1anclem8  37870  cntotbnd  37966  dalemply  39949  dalemsly  39950  dalem5  39962  dalem13  39971  dalem17  39975  dalem55  40022  dalem57  40024  lhpat3  40341  cdleme22aa  40634  aks4d1p1p7  42363  evlselv  42867  jm2.27c  43286  hashnzfz2  44599  supxrubd  45394  suprnmpt  45455  fzisoeu  45585  upbdrech  45590  recnnltrp  45658  uzublem  45711  fmul01  45863  limsupubuzlem  45993  limsupequzmptlem  46009  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  stoweidlem36  46317  stoweidlem41  46322  wallispi2  46354  dirkercncflem1  46384  fourierdlem6  46394  fourierdlem7  46395  fourierdlem19  46407  fourierdlem20  46408  fourierdlem24  46412  fourierdlem25  46413  fourierdlem26  46414  fourierdlem30  46418  fourierdlem31  46419  fourierdlem42  46430  fourierdlem47  46434  fourierdlem48  46435  fourierdlem63  46450  fourierdlem64  46451  fourierdlem65  46452  fourierdlem71  46458  fourierdlem79  46466  fourierdlem89  46476  fourierdlem90  46477  fourierdlem91  46478  fouriersw  46512  etransclem28  46543  etransclem48  46563  hoidmv1lelem1  46872  hoidmv1lelem3  46874  hoidmvlelem1  46876  hoidmvlelem4  46879  bgoldbtbndlem2  48089  gpg3kgrtriexlem4  48369  gpg3kgrtriexlem6  48371  lincresunit3lem2  48763  lincresunit3  48764  resum2sqgt0  48990  amgmwlem  50084