Theorem breqtrrdi 5152

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 2771	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtrdi 5151	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:  enpr2d  9043  pw2eng  9069  undjudom  10158  dju1en  10162  djucomen  10168  djuassen  10169  xpdjuen  10170  infdjuabs  10195  ackbij1lem9  10217  unsnen  10543  1nqenq  10953  gtndiv  12679  xov1plusxeqvd  13531  intfrac2  13898  serle  14100  discr1  14282  faclbnd4lem1  14336  01sqrexlem1  15300  01sqrexlem4  15303  01sqrexlem7  15306  supcvg  15917  ege2le3  16150  eirrlem  16266  ruclem12  16303  bitsfzo  16499  pcprendvds  16906  pcpremul  16909  pcfaclem  16964  infpnlem2  16977  yonedainv  18343  srgbinomlem4  20317  lmcn2  23817  hmph0  23963  icccmplem2  24992  reconnlem2  24996  xrge0tsms  25003  minveclem2  25596  minveclem3b  25598  minveclem4  25602  minveclem6  25604  ivthlem2  25622  ivthlem3  25623  vitalilem2  25779  itg2seq  25912  itg2monolem1  25920  itg2monolem2  25921  itg2monolem3  25922  dveflem  26149  dvferm1lem  26154  dvferm2lem  26156  c1liplem1  26166  lhop1lem  26183  dvcvx  26190  plyeq0lem  26378  radcnvcl  26591  radcnvle  26594  psercnlem1  26599  psercn  26600  pilem3  26627  tangtx  26681  cos02pilt1  26702  cosne0  26705  recosf1o  26711  resinf1o  26712  efif1olem4  26721  logi  26763  logimul  26790  logcnlem3  26820  logf1o2  26826  ang180lem2  26986  heron  27014  acoscos  27069  emcllem7  27177  fsumharmonic  27187  ftalem2  27249  basellem1  27256  basellem2  27257  basellem3  27258  basellem5  27260  bposlem1  27459  bposlem2  27460  bposlem3  27461  lgsdirprm  27506  chebbnd1lem1  27644  chebbnd1lem2  27645  chebbnd1lem3  27646  mulog2sumlem2  27710  pntpbnd1a  27760  pntpbnd1  27761  pntpbnd2  27762  pntibndlem2  27766  pntlemc  27770  pntlemb  27772  pntlemg  27773  pntlemh  27774  pntlemr  27777  ostth2lem2  27809  ostth2lem3  27810  ostth2lem4  27811  ostth3  27813  axsegconlem3  29280  clwlkclwwlk2  30365  siilem1  31214  minvecolem2  31238  minvecolem4  31243  minvecolem5  31244  minvecolem6  31245  nmopcoi  32458  staddi  32609  cycpmco2lem4  33458  cycpmco2lem5  33459  iconstr  34165  hgt750lemd  35044  climlec3  36234  poimirlem26  38325  ftc1anclem8  38379  cntotbnd  38475  dalemply  40456  dalemsly  40457  dalem5  40469  dalem13  40478  dalem17  40482  dalem55  40529  dalem57  40531  lhpat3  40848  cdleme22aa  41141  aks4d1p1p7  42869  evlselv  43349  jm2.27c  43762  hashnzfz2  45059  supxrubd  45859  suprnmpt  45920  fzisoeu  46047  upbdrech  46052  recnnltrp  46120  uzublem  46172  fmul01  46324  limsupubuzlem  46454  limsupequzmptlem  46470  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  stoweidlem36  46778  stoweidlem41  46783  wallispi2  46815  dirkercncflem1  46845  fourierdlem6  46855  fourierdlem7  46856  fourierdlem19  46868  fourierdlem20  46869  fourierdlem24  46873  fourierdlem25  46874  fourierdlem26  46875  fourierdlem30  46879  fourierdlem31  46880  fourierdlem42  46891  fourierdlem47  46895  fourierdlem48  46896  fourierdlem49  46897  fourierdlem63  46911  fourierdlem64  46912  fourierdlem65  46913  fourierdlem71  46919  fourierdlem79  46927  fourierdlem89  46937  fourierdlem90  46938  fourierdlem91  46939  fouriersw  46973  etransclem28  47004  etransclem48  47024  hoidmv1lelem1  47333  hoidmv1lelem3  47335  hoidmvlelem1  47337  hoidmvlelem4  47340  bgoldbtbndlem2  48599  gpg3kgrtriexlem4  48879  gpg3kgrtriexlem6  48881  lincresunit3lem2  49288  lincresunit3  49289  resum2sqgt0  49515  amgmwlem  50677