Theorem breqtrrdi 5151

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  enpr2d  9058  pw2eng  9084  undjudom  10173  dju1en  10177  djucomen  10183  djuassen  10184  xpdjuen  10185  infdjuabs  10210  ackbij1lem9  10232  unsnen  10564  1nqenq  10974  gtndiv  12701  xov1plusxeqvd  13553  intfrac2  13921  serle  14123  discr1  14305  faclbnd4lem1  14359  01sqrexlem1  15331  01sqrexlem4  15334  01sqrexlem7  15337  supcvg  15947  ege2le3  16180  eirrlem  16296  ruclem12  16333  bitsfzo  16529  pcprendvds  16936  pcpremul  16939  pcfaclem  16994  infpnlem2  17007  yonedainv  18373  srgbinomlem4  20369  lmcn2  23876  hmph0  24022  icccmplem2  25051  reconnlem2  25055  xrge0tsms  25062  minveclem2  25655  minveclem3b  25657  minveclem4  25661  minveclem6  25663  ivthlem2  25681  ivthlem3  25682  vitalilem2  25838  itg2seq  25971  itg2monolem1  25979  itg2monolem2  25980  itg2monolem3  25981  dveflem  26208  dvferm1lem  26213  dvferm2lem  26215  c1liplem1  26225  lhop1lem  26242  dvcvx  26249  plyeq0lem  26437  radcnvcl  26650  radcnvle  26653  psercnlem1  26658  psercn  26659  pilem3  26686  tangtx  26740  cos02pilt1  26761  cosne0  26764  recosf1o  26770  resinf1o  26771  efif1olem4  26780  logi  26822  logimul  26849  logcnlem3  26879  logf1o2  26885  ang180lem2  27045  heron  27073  acoscos  27128  emcllem7  27236  fsumharmonic  27246  ftalem2  27308  basellem1  27315  basellem2  27316  basellem3  27317  basellem5  27319  bposlem1  27518  bposlem2  27519  bposlem3  27520  lgsdirprm  27565  chebbnd1lem1  27703  chebbnd1lem2  27704  chebbnd1lem3  27705  mulog2sumlem2  27769  pntpbnd1a  27819  pntpbnd1  27820  pntpbnd2  27821  pntibndlem2  27825  pntlemc  27829  pntlemb  27831  pntlemg  27832  pntlemh  27833  pntlemr  27836  ostth2lem2  27868  ostth2lem3  27869  ostth2lem4  27870  ostth3  27872  axsegconlem3  29362  clwlkclwwlk2  30459  siilem1  31318  minvecolem2  31342  minvecolem4  31347  minvecolem5  31348  minvecolem6  31349  nmopcoi  32562  staddi  32713  cycpmco2lem4  33556  cycpmco2lem5  33557  iconstr  34263  hgt750lemd  35143  climlec3  36300  poimirlem26  38382  ftc1anclem8  38436  cntotbnd  38533  dalemply  40514  dalemsly  40515  dalem5  40527  dalem13  40536  dalem17  40540  dalem55  40587  dalem57  40589  lhpat3  40906  cdleme22aa  41199  aks4d1p1p7  42927  evlselv  43422  jm2.27c  43835  hashnzfz2  45132  supxrubd  45932  suprnmpt  45993  fzisoeu  46120  upbdrech  46125  recnnltrp  46193  uzublem  46245  fmul01  46397  limsupubuzlem  46527  limsupequzmptlem  46543  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  stoweidlem36  46851  stoweidlem41  46856  wallispi2  46888  dirkercncflem1  46918  fourierdlem6  46928  fourierdlem7  46929  fourierdlem19  46941  fourierdlem20  46942  fourierdlem24  46946  fourierdlem25  46947  fourierdlem26  46948  fourierdlem30  46952  fourierdlem31  46953  fourierdlem42  46964  fourierdlem47  46968  fourierdlem48  46969  fourierdlem49  46970  fourierdlem63  46984  fourierdlem64  46985  fourierdlem65  46986  fourierdlem71  46992  fourierdlem79  47000  fourierdlem89  47010  fourierdlem90  47011  fourierdlem91  47012  fouriersw  47046  etransclem28  47077  etransclem48  47097  hoidmv1lelem1  47406  hoidmv1lelem3  47408  hoidmvlelem1  47410  hoidmvlelem4  47413  bgoldbtbndlem2  48709  gpg3kgrtriexlem4  48989  gpg3kgrtriexlem6  48991  lincresunit3lem2  49397  lincresunit3  49398  resum2sqgt0  49624  amgmwlem  50807