Theorem breqtrrdi 5144

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  enpr2d  8997  enpr2dOLD  8998  pw2eng  9024  undjudom  10099  dju1en  10103  djucomen  10109  djuassen  10110  xpdjuen  10111  infdjuabs  10136  ackbij1lem9  10158  unsnen  10484  1nqenq  10893  gtndiv  12589  xov1plusxeqvd  13437  intfrac2  13798  serle  14000  discr1  14182  faclbnd4lem1  14236  01sqrexlem1  15185  01sqrexlem4  15188  01sqrexlem7  15191  supcvg  15799  ege2le3  16033  eirrlem  16149  ruclem12  16186  bitsfzo  16382  pcprendvds  16788  pcpremul  16791  pcfaclem  16846  infpnlem2  16859  yonedainv  18223  srgbinomlem4  20150  lmcn2  23570  hmph0  23716  icccmplem2  24746  reconnlem2  24750  xrge0tsms  24757  minveclem2  25360  minveclem3b  25362  minveclem4  25366  minveclem6  25368  ivthlem2  25387  ivthlem3  25388  vitalilem2  25544  itg2seq  25677  itg2monolem1  25685  itg2monolem2  25686  itg2monolem3  25687  dveflem  25917  dvferm1lem  25922  dvferm2lem  25924  c1liplem1  25935  lhop1lem  25952  dvcvx  25959  plyeq0lem  26149  radcnvcl  26360  radcnvle  26363  psercnlem1  26369  psercn  26370  pilem3  26397  tangtx  26448  cos02pilt1  26469  cosne0  26472  recosf1o  26478  resinf1o  26479  efif1olem4  26488  logi  26530  logimul  26557  logcnlem3  26587  logf1o2  26593  ang180lem2  26754  heron  26782  acoscos  26837  emcllem7  26946  fsumharmonic  26956  ftalem2  27018  basellem1  27025  basellem2  27026  basellem3  27027  basellem5  27029  bposlem1  27229  bposlem2  27230  bposlem3  27231  lgsdirprm  27276  chebbnd1lem1  27414  chebbnd1lem2  27415  chebbnd1lem3  27416  mulog2sumlem2  27480  pntpbnd1a  27530  pntpbnd1  27531  pntpbnd2  27532  pntibndlem2  27536  pntlemc  27540  pntlemb  27542  pntlemg  27543  pntlemh  27544  pntlemr  27547  ostth2lem2  27579  ostth2lem3  27580  ostth2lem4  27581  ostth3  27583  axsegconlem3  28900  clwlkclwwlk2  29983  siilem1  30831  minvecolem2  30855  minvecolem4  30860  minvecolem5  30861  minvecolem6  30862  nmopcoi  32075  staddi  32226  cycpmco2lem4  33102  cycpmco2lem5  33103  iconstr  33750  hgt750lemd  34633  climlec3  35715  poimirlem26  37634  ftc1anclem8  37688  cntotbnd  37784  dalemply  39642  dalemsly  39643  dalem5  39655  dalem13  39664  dalem17  39668  dalem55  39715  dalem57  39717  lhpat3  40034  cdleme22aa  40327  aks4d1p1p7  42056  evlselv  42569  jm2.27c  42990  hashnzfz2  44304  supxrubd  45101  suprnmpt  45162  fzisoeu  45292  upbdrech  45297  recnnltrp  45367  uzublem  45420  fmul01  45572  limsupubuzlem  45704  limsupequzmptlem  45720  ioodvbdlimc1lem2  45924  ioodvbdlimc2lem  45926  stoweidlem36  46028  stoweidlem41  46033  wallispi2  46065  dirkercncflem1  46095  fourierdlem6  46105  fourierdlem7  46106  fourierdlem19  46118  fourierdlem20  46119  fourierdlem24  46123  fourierdlem25  46124  fourierdlem26  46125  fourierdlem30  46129  fourierdlem31  46130  fourierdlem42  46141  fourierdlem47  46145  fourierdlem48  46146  fourierdlem63  46161  fourierdlem64  46162  fourierdlem65  46163  fourierdlem71  46169  fourierdlem79  46177  fourierdlem89  46187  fourierdlem90  46188  fourierdlem91  46189  fouriersw  46223  etransclem28  46254  etransclem48  46274  hoidmv1lelem1  46583  hoidmv1lelem3  46585  hoidmvlelem1  46587  hoidmvlelem4  46590  bgoldbtbndlem2  47801  gpg3kgrtriexlem4  48071  gpg3kgrtriexlem6  48073  lincresunit3lem2  48463  lincresunit3  48464  resum2sqgt0  48690  amgmwlem  49785