Theorem breqtrrdi 5131

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  enpr2d  8970  pw2eng  8996  undjudom  10059  dju1en  10063  djucomen  10069  djuassen  10070  xpdjuen  10071  infdjuabs  10096  ackbij1lem9  10118  unsnen  10444  1nqenq  10853  gtndiv  12550  xov1plusxeqvd  13398  intfrac2  13762  serle  13964  discr1  14146  faclbnd4lem1  14200  01sqrexlem1  15149  01sqrexlem4  15152  01sqrexlem7  15155  supcvg  15763  ege2le3  15997  eirrlem  16113  ruclem12  16150  bitsfzo  16346  pcprendvds  16752  pcpremul  16755  pcfaclem  16810  infpnlem2  16823  yonedainv  18187  srgbinomlem4  20147  lmcn2  23564  hmph0  23710  icccmplem2  24739  reconnlem2  24743  xrge0tsms  24750  minveclem2  25353  minveclem3b  25355  minveclem4  25359  minveclem6  25361  ivthlem2  25380  ivthlem3  25381  vitalilem2  25537  itg2seq  25670  itg2monolem1  25678  itg2monolem2  25679  itg2monolem3  25680  dveflem  25910  dvferm1lem  25915  dvferm2lem  25917  c1liplem1  25928  lhop1lem  25945  dvcvx  25952  plyeq0lem  26142  radcnvcl  26353  radcnvle  26356  psercnlem1  26362  psercn  26363  pilem3  26390  tangtx  26441  cos02pilt1  26462  cosne0  26465  recosf1o  26471  resinf1o  26472  efif1olem4  26481  logi  26523  logimul  26550  logcnlem3  26580  logf1o2  26586  ang180lem2  26747  heron  26775  acoscos  26830  emcllem7  26939  fsumharmonic  26949  ftalem2  27011  basellem1  27018  basellem2  27019  basellem3  27020  basellem5  27022  bposlem1  27222  bposlem2  27223  bposlem3  27224  lgsdirprm  27269  chebbnd1lem1  27407  chebbnd1lem2  27408  chebbnd1lem3  27409  mulog2sumlem2  27473  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem2  27529  pntlemc  27533  pntlemb  27535  pntlemg  27536  pntlemh  27537  pntlemr  27540  ostth2lem2  27572  ostth2lem3  27573  ostth2lem4  27574  ostth3  27576  axsegconlem3  28897  clwlkclwwlk2  29983  siilem1  30831  minvecolem2  30855  minvecolem4  30860  minvecolem5  30861  minvecolem6  30862  nmopcoi  32075  staddi  32226  cycpmco2lem4  33098  cycpmco2lem5  33099  iconstr  33779  hgt750lemd  34661  climlec3  35778  poimirlem26  37685  ftc1anclem8  37739  cntotbnd  37835  dalemply  39752  dalemsly  39753  dalem5  39765  dalem13  39774  dalem17  39778  dalem55  39825  dalem57  39827  lhpat3  40144  cdleme22aa  40437  aks4d1p1p7  42166  evlselv  42679  jm2.27c  43099  hashnzfz2  44413  supxrubd  45209  suprnmpt  45270  fzisoeu  45400  upbdrech  45405  recnnltrp  45474  uzublem  45527  fmul01  45679  limsupubuzlem  45809  limsupequzmptlem  45825  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  stoweidlem36  46133  stoweidlem41  46138  wallispi2  46170  dirkercncflem1  46200  fourierdlem6  46210  fourierdlem7  46211  fourierdlem19  46223  fourierdlem20  46224  fourierdlem24  46228  fourierdlem25  46229  fourierdlem26  46230  fourierdlem30  46234  fourierdlem31  46235  fourierdlem42  46246  fourierdlem47  46250  fourierdlem48  46251  fourierdlem63  46266  fourierdlem64  46267  fourierdlem65  46268  fourierdlem71  46274  fourierdlem79  46282  fourierdlem89  46292  fourierdlem90  46293  fourierdlem91  46294  fouriersw  46328  etransclem28  46359  etransclem48  46379  hoidmv1lelem1  46688  hoidmv1lelem3  46690  hoidmvlelem1  46692  hoidmvlelem4  46695  bgoldbtbndlem2  47905  gpg3kgrtriexlem4  48185  gpg3kgrtriexlem6  48187  lincresunit3lem2  48580  lincresunit3  48581  resum2sqgt0  48807  amgmwlem  49902