Theorem breqtrrdi 5117

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

Syntax hints:   → wi 4   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  enpr2d  8989  pw2eng  9015  undjudom  10085  dju1en  10089  djucomen  10095  djuassen  10096  xpdjuen  10097  infdjuabs  10122  ackbij1lem9  10144  unsnen  10470  1nqenq  10880  gtndiv  12601  xov1plusxeqvd  13446  intfrac2  13812  serle  14014  discr1  14196  faclbnd4lem1  14250  01sqrexlem1  15199  01sqrexlem4  15202  01sqrexlem7  15205  supcvg  15816  ege2le3  16050  eirrlem  16166  ruclem12  16203  bitsfzo  16399  pcprendvds  16806  pcpremul  16809  pcfaclem  16864  infpnlem2  16877  yonedainv  18242  srgbinomlem4  20205  lmcn2  23636  hmph0  23782  icccmplem2  24811  reconnlem2  24815  xrge0tsms  24822  minveclem2  25415  minveclem3b  25417  minveclem4  25421  minveclem6  25423  ivthlem2  25441  ivthlem3  25442  vitalilem2  25598  itg2seq  25731  itg2monolem1  25739  itg2monolem2  25740  itg2monolem3  25741  dveflem  25968  dvferm1lem  25973  dvferm2lem  25975  c1liplem1  25985  lhop1lem  26002  dvcvx  26009  plyeq0lem  26197  radcnvcl  26404  radcnvle  26407  psercnlem1  26412  psercn  26413  pilem3  26440  tangtx  26491  cos02pilt1  26512  cosne0  26515  recosf1o  26521  resinf1o  26522  efif1olem4  26531  logi  26573  logimul  26600  logcnlem3  26630  logf1o2  26636  ang180lem2  26796  heron  26824  acoscos  26879  emcllem7  26987  fsumharmonic  26997  ftalem2  27059  basellem1  27066  basellem2  27067  basellem3  27068  basellem5  27070  bposlem1  27269  bposlem2  27270  bposlem3  27271  lgsdirprm  27316  chebbnd1lem1  27454  chebbnd1lem2  27455  chebbnd1lem3  27456  mulog2sumlem2  27520  pntpbnd1a  27570  pntpbnd1  27571  pntpbnd2  27572  pntibndlem2  27576  pntlemc  27580  pntlemb  27582  pntlemg  27583  pntlemh  27584  pntlemr  27587  ostth2lem2  27619  ostth2lem3  27620  ostth2lem4  27621  ostth3  27623  axsegconlem3  29010  clwlkclwwlk2  30095  siilem1  30944  minvecolem2  30968  minvecolem4  30973  minvecolem5  30974  minvecolem6  30975  nmopcoi  32188  staddi  32339  cycpmco2lem4  33214  cycpmco2lem5  33215  iconstr  33962  hgt750lemd  34844  climlec3  35977  poimirlem26  38028  ftc1anclem8  38082  cntotbnd  38178  dalemply  40161  dalemsly  40162  dalem5  40174  dalem13  40183  dalem17  40187  dalem55  40234  dalem57  40236  lhpat3  40553  cdleme22aa  40846  aks4d1p1p7  42574  evlselv  43054  jm2.27c  43467  hashnzfz2  44780  supxrubd  45574  suprnmpt  45635  fzisoeu  45762  upbdrech  45767  recnnltrp  45835  uzublem  45887  fmul01  46039  limsupubuzlem  46169  limsupequzmptlem  46185  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  stoweidlem36  46493  stoweidlem41  46498  wallispi2  46530  dirkercncflem1  46560  fourierdlem6  46570  fourierdlem7  46571  fourierdlem19  46583  fourierdlem20  46584  fourierdlem24  46588  fourierdlem25  46589  fourierdlem26  46590  fourierdlem30  46594  fourierdlem31  46595  fourierdlem42  46606  fourierdlem47  46610  fourierdlem48  46611  fourierdlem63  46626  fourierdlem64  46627  fourierdlem65  46628  fourierdlem71  46634  fourierdlem79  46642  fourierdlem89  46652  fourierdlem90  46653  fourierdlem91  46654  fouriersw  46688  etransclem28  46719  etransclem48  46739  hoidmv1lelem1  47048  hoidmv1lelem3  47050  hoidmvlelem1  47052  hoidmvlelem4  47055  bgoldbtbndlem2  48311  gpg3kgrtriexlem4  48591  gpg3kgrtriexlem6  48593  lincresunit3lem2  48985  lincresunit3  48986  resum2sqgt0  49212  amgmwlem  50306