Theorem breqtrrdi 5161

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 5160	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  enpr2d  9061  enpr2dOLD  9062  pw2eng  9090  undjudom  10180  dju1en  10184  djucomen  10190  djuassen  10191  xpdjuen  10192  infdjuabs  10217  ackbij1lem9  10239  unsnen  10565  1nqenq  10974  gtndiv  12668  xov1plusxeqvd  13513  intfrac2  13873  serle  14073  discr1  14255  faclbnd4lem1  14309  01sqrexlem1  15259  01sqrexlem4  15262  01sqrexlem7  15265  supcvg  15870  ege2le3  16104  eirrlem  16220  ruclem12  16257  bitsfzo  16452  pcprendvds  16858  pcpremul  16861  pcfaclem  16916  infpnlem2  16929  yonedainv  18291  srgbinomlem4  20187  lmcn2  23585  hmph0  23731  icccmplem2  24761  reconnlem2  24765  xrge0tsms  24772  minveclem2  25376  minveclem3b  25378  minveclem4  25382  minveclem6  25384  ivthlem2  25403  ivthlem3  25404  vitalilem2  25560  itg2seq  25693  itg2monolem1  25701  itg2monolem2  25702  itg2monolem3  25703  dveflem  25933  dvferm1lem  25938  dvferm2lem  25940  c1liplem1  25951  lhop1lem  25968  dvcvx  25975  plyeq0lem  26165  radcnvcl  26376  radcnvle  26379  psercnlem1  26385  psercn  26386  pilem3  26413  tangtx  26464  cos02pilt1  26485  cosne0  26488  recosf1o  26494  resinf1o  26495  efif1olem4  26504  logi  26546  logimul  26573  logcnlem3  26603  logf1o2  26609  ang180lem2  26770  heron  26798  acoscos  26853  emcllem7  26962  fsumharmonic  26972  ftalem2  27034  basellem1  27041  basellem2  27042  basellem3  27043  basellem5  27045  bposlem1  27245  bposlem2  27246  bposlem3  27247  lgsdirprm  27292  chebbnd1lem1  27430  chebbnd1lem2  27431  chebbnd1lem3  27432  mulog2sumlem2  27496  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntibndlem2  27552  pntlemc  27556  pntlemb  27558  pntlemg  27559  pntlemh  27560  pntlemr  27563  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ostth3  27599  axsegconlem3  28844  clwlkclwwlk2  29930  siilem1  30778  minvecolem2  30802  minvecolem4  30807  minvecolem5  30808  minvecolem6  30809  nmopcoi  32022  staddi  32173  cycpmco2lem4  33086  cycpmco2lem5  33087  iconstr  33746  hgt750lemd  34626  climlec3  35697  poimirlem26  37616  ftc1anclem8  37670  cntotbnd  37766  dalemply  39619  dalemsly  39620  dalem5  39632  dalem13  39641  dalem17  39645  dalem55  39692  dalem57  39694  lhpat3  40011  cdleme22aa  40304  aks4d1p1p7  42033  evlselv  42557  jm2.27c  42978  hashnzfz2  44293  supxrubd  45085  suprnmpt  45146  fzisoeu  45277  upbdrech  45282  recnnltrp  45352  uzublem  45405  fmul01  45557  limsupubuzlem  45689  limsupequzmptlem  45705  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  stoweidlem36  46013  stoweidlem41  46018  wallispi2  46050  dirkercncflem1  46080  fourierdlem6  46090  fourierdlem7  46091  fourierdlem19  46103  fourierdlem20  46104  fourierdlem24  46108  fourierdlem25  46109  fourierdlem26  46110  fourierdlem30  46114  fourierdlem31  46115  fourierdlem42  46126  fourierdlem47  46130  fourierdlem48  46131  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem71  46154  fourierdlem79  46162  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fouriersw  46208  etransclem28  46239  etransclem48  46259  hoidmv1lelem1  46568  hoidmv1lelem3  46570  hoidmvlelem1  46572  hoidmvlelem4  46575  bgoldbtbndlem2  47768  gpg3kgrtriexlem4  48036  gpg3kgrtriexlem6  48038  lincresunit3lem2  48404  lincresunit3  48405  resum2sqgt0  48635  amgmwlem  49614