Theorem breqtrrdi 5072

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

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  enpr2d  8580  pw2eng  8606  undjudom  9578  dju1en  9582  djucomen  9588  djuassen  9589  xpdjuen  9590  infdjuabs  9617  ackbij1lem9  9639  unsnen  9964  1nqenq  10373  gtndiv  12047  xov1plusxeqvd  12876  intfrac2  13221  serle  13421  discr1  13596  faclbnd4lem1  13649  sqrlem1  14594  sqrlem4  14597  sqrlem7  14600  supcvg  15203  ege2le3  15435  eirrlem  15549  ruclem12  15586  bitsfzo  15774  pcprendvds  16167  pcpremul  16170  pcfaclem  16224  infpnlem2  16237  yonedainv  17523  srgbinomlem4  19286  lmcn2  22254  hmph0  22400  icccmplem2  23428  reconnlem2  23432  xrge0tsms  23439  minveclem2  24030  minveclem3b  24032  minveclem4  24036  minveclem6  24038  ivthlem2  24056  ivthlem3  24057  vitalilem2  24213  itg2seq  24346  itg2monolem1  24354  itg2monolem2  24355  itg2monolem3  24356  dveflem  24582  dvferm1lem  24587  dvferm2lem  24589  c1liplem1  24599  lhop1lem  24616  dvcvx  24623  plyeq0lem  24807  radcnvcl  25012  radcnvle  25015  psercnlem1  25020  psercn  25021  pilem3  25048  tangtx  25098  cos02pilt1  25118  cosne0  25121  recosf1o  25127  resinf1o  25128  efif1olem4  25137  logimul  25205  logcnlem3  25235  logf1o2  25241  ang180lem2  25396  heron  25424  acoscos  25479  emcllem7  25587  fsumharmonic  25597  ftalem2  25659  basellem1  25666  basellem2  25667  basellem3  25668  basellem5  25670  bposlem1  25868  bposlem2  25869  bposlem3  25870  lgsdirprm  25915  chebbnd1lem1  26053  chebbnd1lem2  26054  chebbnd1lem3  26055  mulog2sumlem2  26119  pntpbnd1a  26169  pntpbnd1  26170  pntpbnd2  26171  pntibndlem2  26175  pntlemc  26179  pntlemb  26181  pntlemg  26182  pntlemh  26183  pntlemr  26186  ostth2lem2  26218  ostth2lem3  26219  ostth2lem4  26220  ostth3  26222  axsegconlem3  26713  clwlkclwwlk2  27788  siilem1  28634  minvecolem2  28658  minvecolem4  28663  minvecolem5  28664  minvecolem6  28665  nmopcoi  29878  staddi  30029  cycpmco2lem4  30821  cycpmco2lem5  30822  hgt750lemd  32029  climlec3  33078  logi  33079  poimirlem26  35083  ftc1anclem8  35137  cntotbnd  35234  dalemply  36950  dalemsly  36951  dalem5  36963  dalem13  36972  dalem17  36976  dalem55  37023  dalem57  37025  lhpat3  37342  cdleme22aa  37635  jm2.27c  39948  hashnzfz2  41025  supxrubd  41749  suprnmpt  41798  fzisoeu  41932  upbdrech  41937  recnnltrp  42009  uzublem  42067  fmul01  42222  limsupubuzlem  42354  limsupequzmptlem  42370  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  stoweidlem36  42678  stoweidlem41  42683  wallispi2  42715  dirkercncflem1  42745  fourierdlem6  42755  fourierdlem7  42756  fourierdlem19  42768  fourierdlem20  42769  fourierdlem24  42773  fourierdlem25  42774  fourierdlem26  42775  fourierdlem30  42779  fourierdlem31  42780  fourierdlem42  42791  fourierdlem47  42795  fourierdlem48  42796  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem71  42819  fourierdlem79  42827  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fouriersw  42873  etransclem28  42904  etransclem48  42924  hoidmv1lelem1  43230  hoidmv1lelem3  43232  hoidmvlelem1  43234  hoidmvlelem4  43237  bgoldbtbndlem2  44324  lincresunit3lem2  44889  lincresunit3  44890  resum2sqgt0  45121  amgmwlem  45330