Theorem breqtrrdi 5189

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

Syntax hints:   → wi 4   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  enpr2d  9087  enpr2dOLD  9088  pw2eng  9116  undjudom  10205  dju1en  10209  djucomen  10215  djuassen  10216  xpdjuen  10217  infdjuabs  10242  ackbij1lem9  10264  unsnen  10590  1nqenq  10999  gtndiv  12692  xov1plusxeqvd  13534  intfrac2  13894  serle  14094  discr1  14274  faclbnd4lem1  14328  01sqrexlem1  15277  01sqrexlem4  15280  01sqrexlem7  15283  supcvg  15888  ege2le3  16122  eirrlem  16236  ruclem12  16273  bitsfzo  16468  pcprendvds  16873  pcpremul  16876  pcfaclem  16931  infpnlem2  16944  yonedainv  18337  srgbinomlem4  20246  lmcn2  23672  hmph0  23818  icccmplem2  24858  reconnlem2  24862  xrge0tsms  24869  minveclem2  25473  minveclem3b  25475  minveclem4  25479  minveclem6  25481  ivthlem2  25500  ivthlem3  25501  vitalilem2  25657  itg2seq  25791  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  dveflem  26031  dvferm1lem  26036  dvferm2lem  26038  c1liplem1  26049  lhop1lem  26066  dvcvx  26073  plyeq0lem  26263  radcnvcl  26474  radcnvle  26477  psercnlem1  26483  psercn  26484  pilem3  26511  tangtx  26561  cos02pilt1  26582  cosne0  26585  recosf1o  26591  resinf1o  26592  efif1olem4  26601  logi  26643  logimul  26670  logcnlem3  26700  logf1o2  26706  ang180lem2  26867  heron  26895  acoscos  26950  emcllem7  27059  fsumharmonic  27069  ftalem2  27131  basellem1  27138  basellem2  27139  basellem3  27140  basellem5  27142  bposlem1  27342  bposlem2  27343  bposlem3  27344  lgsdirprm  27389  chebbnd1lem1  27527  chebbnd1lem2  27528  chebbnd1lem3  27529  mulog2sumlem2  27593  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntibndlem2  27649  pntlemc  27653  pntlemb  27655  pntlemg  27656  pntlemh  27657  pntlemr  27660  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  ostth3  27696  axsegconlem3  28948  clwlkclwwlk2  30031  siilem1  30879  minvecolem2  30903  minvecolem4  30908  minvecolem5  30909  minvecolem6  30910  nmopcoi  32123  staddi  32274  cycpmco2lem4  33131  cycpmco2lem5  33132  hgt750lemd  34641  climlec3  35713  poimirlem26  37632  ftc1anclem8  37686  cntotbnd  37782  dalemply  39636  dalemsly  39637  dalem5  39649  dalem13  39658  dalem17  39662  dalem55  39709  dalem57  39711  lhpat3  40028  cdleme22aa  40321  aks4d1p1p7  42055  evlselv  42573  jm2.27c  42995  hashnzfz2  44316  supxrubd  45052  suprnmpt  45116  fzisoeu  45250  upbdrech  45255  recnnltrp  45326  uzublem  45379  fmul01  45535  limsupubuzlem  45667  limsupequzmptlem  45683  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem36  45991  stoweidlem41  45996  wallispi2  46028  dirkercncflem1  46058  fourierdlem6  46068  fourierdlem7  46069  fourierdlem19  46081  fourierdlem20  46082  fourierdlem24  46086  fourierdlem25  46087  fourierdlem26  46088  fourierdlem30  46092  fourierdlem31  46093  fourierdlem42  46104  fourierdlem47  46108  fourierdlem48  46109  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem71  46132  fourierdlem79  46140  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fouriersw  46186  etransclem28  46217  etransclem48  46237  hoidmv1lelem1  46546  hoidmv1lelem3  46548  hoidmvlelem1  46550  hoidmvlelem4  46553  bgoldbtbndlem2  47730  lincresunit3lem2  48325  lincresunit3  48326  resum2sqgt0  48556  amgmwlem  49032