Theorem breqtrrdi 5142

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5100

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  enpr2d  8999  pw2eng  9025  undjudom  10092  dju1en  10096  djucomen  10102  djuassen  10103  xpdjuen  10104  infdjuabs  10129  ackbij1lem9  10151  unsnen  10477  1nqenq  10887  gtndiv  12583  xov1plusxeqvd  13428  intfrac2  13792  serle  13994  discr1  14176  faclbnd4lem1  14230  01sqrexlem1  15179  01sqrexlem4  15182  01sqrexlem7  15185  supcvg  15793  ege2le3  16027  eirrlem  16143  ruclem12  16180  bitsfzo  16376  pcprendvds  16782  pcpremul  16785  pcfaclem  16840  infpnlem2  16853  yonedainv  18218  srgbinomlem4  20181  lmcn2  23610  hmph0  23756  icccmplem2  24785  reconnlem2  24789  xrge0tsms  24796  minveclem2  25399  minveclem3b  25401  minveclem4  25405  minveclem6  25407  ivthlem2  25426  ivthlem3  25427  vitalilem2  25583  itg2seq  25716  itg2monolem1  25724  itg2monolem2  25725  itg2monolem3  25726  dveflem  25956  dvferm1lem  25961  dvferm2lem  25963  c1liplem1  25974  lhop1lem  25991  dvcvx  25998  plyeq0lem  26188  radcnvcl  26399  radcnvle  26402  psercnlem1  26408  psercn  26409  pilem3  26436  tangtx  26487  cos02pilt1  26508  cosne0  26511  recosf1o  26517  resinf1o  26518  efif1olem4  26527  logi  26569  logimul  26596  logcnlem3  26626  logf1o2  26632  ang180lem2  26793  heron  26821  acoscos  26876  emcllem7  26985  fsumharmonic  26995  ftalem2  27057  basellem1  27064  basellem2  27065  basellem3  27066  basellem5  27068  bposlem1  27268  bposlem2  27269  bposlem3  27270  lgsdirprm  27315  chebbnd1lem1  27453  chebbnd1lem2  27454  chebbnd1lem3  27455  mulog2sumlem2  27519  pntpbnd1a  27569  pntpbnd1  27570  pntpbnd2  27571  pntibndlem2  27575  pntlemc  27579  pntlemb  27581  pntlemg  27582  pntlemh  27583  pntlemr  27586  ostth2lem2  27618  ostth2lem3  27619  ostth2lem4  27620  ostth3  27622  axsegconlem3  29010  clwlkclwwlk2  30096  siilem1  30945  minvecolem2  30969  minvecolem4  30974  minvecolem5  30975  minvecolem6  30976  nmopcoi  32189  staddi  32340  cycpmco2lem4  33229  cycpmco2lem5  33230  iconstr  33950  hgt750lemd  34832  climlec3  35956  poimirlem26  37926  ftc1anclem8  37980  cntotbnd  38076  dalemply  40059  dalemsly  40060  dalem5  40072  dalem13  40081  dalem17  40085  dalem55  40132  dalem57  40134  lhpat3  40451  cdleme22aa  40744  aks4d1p1p7  42473  evlselv  42974  jm2.27c  43393  hashnzfz2  44706  supxrubd  45501  suprnmpt  45562  fzisoeu  45691  upbdrech  45696  recnnltrp  45764  uzublem  45817  fmul01  45969  limsupubuzlem  46099  limsupequzmptlem  46115  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  stoweidlem36  46423  stoweidlem41  46428  wallispi2  46460  dirkercncflem1  46490  fourierdlem6  46500  fourierdlem7  46501  fourierdlem19  46513  fourierdlem20  46514  fourierdlem24  46518  fourierdlem25  46519  fourierdlem26  46520  fourierdlem30  46524  fourierdlem31  46525  fourierdlem42  46536  fourierdlem47  46540  fourierdlem48  46541  fourierdlem63  46556  fourierdlem64  46557  fourierdlem65  46558  fourierdlem71  46564  fourierdlem79  46572  fourierdlem89  46582  fourierdlem90  46583  fourierdlem91  46584  fouriersw  46618  etransclem28  46649  etransclem48  46669  hoidmv1lelem1  46978  hoidmv1lelem3  46980  hoidmvlelem1  46982  hoidmvlelem4  46985  bgoldbtbndlem2  48195  gpg3kgrtriexlem4  48475  gpg3kgrtriexlem6  48477  lincresunit3lem2  48869  lincresunit3  48870  resum2sqgt0  49096  amgmwlem  50190