Theorem breqtrrdi 5112

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  enpr2d  8792  pw2eng  8818  undjudom  9854  dju1en  9858  djucomen  9864  djuassen  9865  xpdjuen  9866  infdjuabs  9893  ackbij1lem9  9915  unsnen  10240  1nqenq  10649  gtndiv  12327  xov1plusxeqvd  13159  intfrac2  13506  serle  13706  discr1  13882  faclbnd4lem1  13935  sqrlem1  14882  sqrlem4  14885  sqrlem7  14888  supcvg  15496  ege2le3  15727  eirrlem  15841  ruclem12  15878  bitsfzo  16070  pcprendvds  16469  pcpremul  16472  pcfaclem  16527  infpnlem2  16540  yonedainv  17915  srgbinomlem4  19694  lmcn2  22708  hmph0  22854  icccmplem2  23892  reconnlem2  23896  xrge0tsms  23903  minveclem2  24495  minveclem3b  24497  minveclem4  24501  minveclem6  24503  ivthlem2  24521  ivthlem3  24522  vitalilem2  24678  itg2seq  24812  itg2monolem1  24820  itg2monolem2  24821  itg2monolem3  24822  dveflem  25048  dvferm1lem  25053  dvferm2lem  25055  c1liplem1  25065  lhop1lem  25082  dvcvx  25089  plyeq0lem  25276  radcnvcl  25481  radcnvle  25484  psercnlem1  25489  psercn  25490  pilem3  25517  tangtx  25567  cos02pilt1  25587  cosne0  25590  recosf1o  25596  resinf1o  25597  efif1olem4  25606  logimul  25674  logcnlem3  25704  logf1o2  25710  ang180lem2  25865  heron  25893  acoscos  25948  emcllem7  26056  fsumharmonic  26066  ftalem2  26128  basellem1  26135  basellem2  26136  basellem3  26137  basellem5  26139  bposlem1  26337  bposlem2  26338  bposlem3  26339  lgsdirprm  26384  chebbnd1lem1  26522  chebbnd1lem2  26523  chebbnd1lem3  26524  mulog2sumlem2  26588  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem2  26644  pntlemc  26648  pntlemb  26650  pntlemg  26651  pntlemh  26652  pntlemr  26655  ostth2lem2  26687  ostth2lem3  26688  ostth2lem4  26689  ostth3  26691  axsegconlem3  27190  clwlkclwwlk2  28268  siilem1  29114  minvecolem2  29138  minvecolem4  29143  minvecolem5  29144  minvecolem6  29145  nmopcoi  30358  staddi  30509  cycpmco2lem4  31298  cycpmco2lem5  31299  hgt750lemd  32528  climlec3  33605  logi  33606  poimirlem26  35730  ftc1anclem8  35784  cntotbnd  35881  dalemply  37595  dalemsly  37596  dalem5  37608  dalem13  37617  dalem17  37621  dalem55  37668  dalem57  37670  lhpat3  37987  cdleme22aa  38280  aks4d1p1p7  40010  jm2.27c  40745  hashnzfz2  41828  supxrubd  42552  suprnmpt  42599  fzisoeu  42729  upbdrech  42734  recnnltrp  42806  uzublem  42860  fmul01  43011  limsupubuzlem  43143  limsupequzmptlem  43159  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem36  43467  stoweidlem41  43472  wallispi2  43504  dirkercncflem1  43534  fourierdlem6  43544  fourierdlem7  43545  fourierdlem19  43557  fourierdlem20  43558  fourierdlem24  43562  fourierdlem25  43563  fourierdlem26  43564  fourierdlem30  43568  fourierdlem31  43569  fourierdlem42  43580  fourierdlem47  43584  fourierdlem48  43585  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem71  43608  fourierdlem79  43616  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fouriersw  43662  etransclem28  43693  etransclem48  43713  hoidmv1lelem1  44019  hoidmv1lelem3  44021  hoidmvlelem1  44023  hoidmvlelem4  44026  bgoldbtbndlem2  45146  lincresunit3lem2  45709  lincresunit3  45710  resum2sqgt0  45941  amgmwlem  46392