Theorem breqtrrdi 5185

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 5184	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  enpr2d  9089  enpr2dOLD  9090  pw2eng  9118  undjudom  10208  dju1en  10212  djucomen  10218  djuassen  10219  xpdjuen  10220  infdjuabs  10245  ackbij1lem9  10267  unsnen  10593  1nqenq  11002  gtndiv  12695  xov1plusxeqvd  13538  intfrac2  13898  serle  14098  discr1  14278  faclbnd4lem1  14332  01sqrexlem1  15281  01sqrexlem4  15284  01sqrexlem7  15287  supcvg  15892  ege2le3  16126  eirrlem  16240  ruclem12  16277  bitsfzo  16472  pcprendvds  16878  pcpremul  16881  pcfaclem  16936  infpnlem2  16949  yonedainv  18326  srgbinomlem4  20226  lmcn2  23657  hmph0  23803  icccmplem2  24845  reconnlem2  24849  xrge0tsms  24856  minveclem2  25460  minveclem3b  25462  minveclem4  25466  minveclem6  25468  ivthlem2  25487  ivthlem3  25488  vitalilem2  25644  itg2seq  25777  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  dveflem  26017  dvferm1lem  26022  dvferm2lem  26024  c1liplem1  26035  lhop1lem  26052  dvcvx  26059  plyeq0lem  26249  radcnvcl  26460  radcnvle  26463  psercnlem1  26469  psercn  26470  pilem3  26497  tangtx  26547  cos02pilt1  26568  cosne0  26571  recosf1o  26577  resinf1o  26578  efif1olem4  26587  logi  26629  logimul  26656  logcnlem3  26686  logf1o2  26692  ang180lem2  26853  heron  26881  acoscos  26936  emcllem7  27045  fsumharmonic  27055  ftalem2  27117  basellem1  27124  basellem2  27125  basellem3  27126  basellem5  27128  bposlem1  27328  bposlem2  27329  bposlem3  27330  lgsdirprm  27375  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  mulog2sumlem2  27579  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntibndlem2  27635  pntlemc  27639  pntlemb  27641  pntlemg  27642  pntlemh  27643  pntlemr  27646  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth3  27682  axsegconlem3  28934  clwlkclwwlk2  30022  siilem1  30870  minvecolem2  30894  minvecolem4  30899  minvecolem5  30900  minvecolem6  30901  nmopcoi  32114  staddi  32265  cycpmco2lem4  33149  cycpmco2lem5  33150  hgt750lemd  34663  climlec3  35734  poimirlem26  37653  ftc1anclem8  37707  cntotbnd  37803  dalemply  39656  dalemsly  39657  dalem5  39669  dalem13  39678  dalem17  39682  dalem55  39729  dalem57  39731  lhpat3  40048  cdleme22aa  40341  aks4d1p1p7  42075  evlselv  42597  jm2.27c  43019  hashnzfz2  44340  supxrubd  45118  suprnmpt  45179  fzisoeu  45312  upbdrech  45317  recnnltrp  45388  uzublem  45441  fmul01  45595  limsupubuzlem  45727  limsupequzmptlem  45743  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem36  46051  stoweidlem41  46056  wallispi2  46088  dirkercncflem1  46118  fourierdlem6  46128  fourierdlem7  46129  fourierdlem19  46141  fourierdlem20  46142  fourierdlem24  46146  fourierdlem25  46147  fourierdlem26  46148  fourierdlem30  46152  fourierdlem31  46153  fourierdlem42  46164  fourierdlem47  46168  fourierdlem48  46169  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem71  46192  fourierdlem79  46200  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fouriersw  46246  etransclem28  46277  etransclem48  46297  hoidmv1lelem1  46606  hoidmv1lelem3  46608  hoidmvlelem1  46610  hoidmvlelem4  46613  bgoldbtbndlem2  47793  gpg3kgrtriexlem4  48042  gpg3kgrtriexlem6  48044  lincresunit3lem2  48397  lincresunit3  48398  resum2sqgt0  48628  amgmwlem  49321