Theorem breqtrrdi 5117

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  enpr2d  8847  pw2eng  8874  undjudom  9932  dju1en  9936  djucomen  9942  djuassen  9943  xpdjuen  9944  infdjuabs  9971  ackbij1lem9  9993  unsnen  10318  1nqenq  10727  gtndiv  12406  xov1plusxeqvd  13239  intfrac2  13587  serle  13787  discr1  13963  faclbnd4lem1  14016  sqrlem1  14963  sqrlem4  14966  sqrlem7  14969  supcvg  15577  ege2le3  15808  eirrlem  15922  ruclem12  15959  bitsfzo  16151  pcprendvds  16550  pcpremul  16553  pcfaclem  16608  infpnlem2  16621  yonedainv  18008  srgbinomlem4  19788  lmcn2  22809  hmph0  22955  icccmplem2  23995  reconnlem2  23999  xrge0tsms  24006  minveclem2  24599  minveclem3b  24601  minveclem4  24605  minveclem6  24607  ivthlem2  24625  ivthlem3  24626  vitalilem2  24782  itg2seq  24916  itg2monolem1  24924  itg2monolem2  24925  itg2monolem3  24926  dveflem  25152  dvferm1lem  25157  dvferm2lem  25159  c1liplem1  25169  lhop1lem  25186  dvcvx  25193  plyeq0lem  25380  radcnvcl  25585  radcnvle  25588  psercnlem1  25593  psercn  25594  pilem3  25621  tangtx  25671  cos02pilt1  25691  cosne0  25694  recosf1o  25700  resinf1o  25701  efif1olem4  25710  logimul  25778  logcnlem3  25808  logf1o2  25814  ang180lem2  25969  heron  25997  acoscos  26052  emcllem7  26160  fsumharmonic  26170  ftalem2  26232  basellem1  26239  basellem2  26240  basellem3  26241  basellem5  26243  bposlem1  26441  bposlem2  26442  bposlem3  26443  lgsdirprm  26488  chebbnd1lem1  26626  chebbnd1lem2  26627  chebbnd1lem3  26628  mulog2sumlem2  26692  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntibndlem2  26748  pntlemc  26752  pntlemb  26754  pntlemg  26755  pntlemh  26756  pntlemr  26759  ostth2lem2  26791  ostth2lem3  26792  ostth2lem4  26793  ostth3  26795  axsegconlem3  27296  clwlkclwwlk2  28376  siilem1  29222  minvecolem2  29246  minvecolem4  29251  minvecolem5  29252  minvecolem6  29253  nmopcoi  30466  staddi  30617  cycpmco2lem4  31405  cycpmco2lem5  31406  hgt750lemd  32637  climlec3  33708  logi  33709  poimirlem26  35812  ftc1anclem8  35866  cntotbnd  35963  dalemply  37675  dalemsly  37676  dalem5  37688  dalem13  37697  dalem17  37701  dalem55  37748  dalem57  37750  lhpat3  38067  cdleme22aa  38360  aks4d1p1p7  40089  jm2.27c  40836  hashnzfz2  41946  supxrubd  42670  suprnmpt  42717  fzisoeu  42846  upbdrech  42851  recnnltrp  42923  uzublem  42977  fmul01  43128  limsupubuzlem  43260  limsupequzmptlem  43276  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweidlem36  43584  stoweidlem41  43589  wallispi2  43621  dirkercncflem1  43651  fourierdlem6  43661  fourierdlem7  43662  fourierdlem19  43674  fourierdlem20  43675  fourierdlem24  43679  fourierdlem25  43680  fourierdlem26  43681  fourierdlem30  43685  fourierdlem31  43686  fourierdlem42  43697  fourierdlem47  43701  fourierdlem48  43702  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem71  43725  fourierdlem79  43733  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fouriersw  43779  etransclem28  43810  etransclem48  43830  hoidmv1lelem1  44136  hoidmv1lelem3  44138  hoidmvlelem1  44140  hoidmvlelem4  44143  bgoldbtbndlem2  45269  lincresunit3lem2  45832  lincresunit3  45833  resum2sqgt0  46064  amgmwlem  46517