Theorem breqtrrdi 5208

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  enpr2d  9115  enpr2dOLD  9116  pw2eng  9144  undjudom  10237  dju1en  10241  djucomen  10247  djuassen  10248  xpdjuen  10249  infdjuabs  10274  ackbij1lem9  10296  unsnen  10622  1nqenq  11031  gtndiv  12720  xov1plusxeqvd  13558  intfrac2  13909  serle  14108  discr1  14288  faclbnd4lem1  14342  01sqrexlem1  15291  01sqrexlem4  15294  01sqrexlem7  15297  supcvg  15904  ege2le3  16138  eirrlem  16252  ruclem12  16289  bitsfzo  16481  pcprendvds  16887  pcpremul  16890  pcfaclem  16945  infpnlem2  16958  yonedainv  18351  srgbinomlem4  20256  lmcn2  23678  hmph0  23824  icccmplem2  24864  reconnlem2  24868  xrge0tsms  24875  minveclem2  25479  minveclem3b  25481  minveclem4  25485  minveclem6  25487  ivthlem2  25506  ivthlem3  25507  vitalilem2  25663  itg2seq  25797  itg2monolem1  25805  itg2monolem2  25806  itg2monolem3  25807  dveflem  26037  dvferm1lem  26042  dvferm2lem  26044  c1liplem1  26055  lhop1lem  26072  dvcvx  26079  plyeq0lem  26269  radcnvcl  26478  radcnvle  26481  psercnlem1  26487  psercn  26488  pilem3  26515  tangtx  26565  cos02pilt1  26586  cosne0  26589  recosf1o  26595  resinf1o  26596  efif1olem4  26605  logi  26647  logimul  26674  logcnlem3  26704  logf1o2  26710  ang180lem2  26871  heron  26899  acoscos  26954  emcllem7  27063  fsumharmonic  27073  ftalem2  27135  basellem1  27142  basellem2  27143  basellem3  27144  basellem5  27146  bposlem1  27346  bposlem2  27347  bposlem3  27348  lgsdirprm  27393  chebbnd1lem1  27531  chebbnd1lem2  27532  chebbnd1lem3  27533  mulog2sumlem2  27597  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntibndlem2  27653  pntlemc  27657  pntlemb  27659  pntlemg  27660  pntlemh  27661  pntlemr  27664  ostth2lem2  27696  ostth2lem3  27697  ostth2lem4  27698  ostth3  27700  axsegconlem3  28952  clwlkclwwlk2  30035  siilem1  30883  minvecolem2  30907  minvecolem4  30912  minvecolem5  30913  minvecolem6  30914  nmopcoi  32127  staddi  32278  cycpmco2lem4  33122  cycpmco2lem5  33123  hgt750lemd  34625  climlec3  35696  poimirlem26  37606  ftc1anclem8  37660  cntotbnd  37756  dalemply  39611  dalemsly  39612  dalem5  39624  dalem13  39633  dalem17  39637  dalem55  39684  dalem57  39686  lhpat3  40003  cdleme22aa  40296  aks4d1p1p7  42031  evlselv  42542  jm2.27c  42964  hashnzfz2  44290  supxrubd  45015  suprnmpt  45081  fzisoeu  45215  upbdrech  45220  recnnltrp  45292  uzublem  45345  fmul01  45501  limsupubuzlem  45633  limsupequzmptlem  45649  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem36  45957  stoweidlem41  45962  wallispi2  45994  dirkercncflem1  46024  fourierdlem6  46034  fourierdlem7  46035  fourierdlem19  46047  fourierdlem20  46048  fourierdlem24  46052  fourierdlem25  46053  fourierdlem26  46054  fourierdlem30  46058  fourierdlem31  46059  fourierdlem42  46070  fourierdlem47  46074  fourierdlem48  46075  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem71  46098  fourierdlem79  46106  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fouriersw  46152  etransclem28  46183  etransclem48  46203  hoidmv1lelem1  46512  hoidmv1lelem3  46514  hoidmvlelem1  46516  hoidmvlelem4  46519  bgoldbtbndlem2  47680  lincresunit3lem2  48209  lincresunit3  48210  resum2sqgt0  48441  amgmwlem  48896