Theorem breqtrrdi 5108

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  enpr2d  8597  pw2eng  8623  undjudom  9593  dju1en  9597  djucomen  9603  djuassen  9604  xpdjuen  9605  infdjuabs  9628  ackbij1lem9  9650  unsnen  9975  1nqenq  10384  gtndiv  12060  xov1plusxeqvd  12885  intfrac2  13227  serle  13426  discr1  13601  faclbnd4lem1  13654  sqrlem1  14602  sqrlem4  14605  sqrlem7  14608  supcvg  15211  ege2le3  15443  eirrlem  15557  ruclem12  15594  bitsfzo  15784  pcprendvds  16177  pcpremul  16180  pcfaclem  16234  infpnlem2  16247  yonedainv  17531  srgbinomlem4  19293  lmcn2  22257  hmph0  22403  icccmplem2  23431  reconnlem2  23435  xrge0tsms  23442  minveclem2  24029  minveclem3b  24031  minveclem4  24035  minveclem6  24037  ivthlem2  24053  ivthlem3  24054  vitalilem2  24210  itg2seq  24343  itg2monolem1  24351  itg2monolem2  24352  itg2monolem3  24353  dveflem  24576  dvferm1lem  24581  dvferm2lem  24583  c1liplem1  24593  lhop1lem  24610  dvcvx  24617  plyeq0lem  24800  radcnvcl  25005  radcnvle  25008  psercnlem1  25013  psercn  25014  pilem3  25041  tangtx  25091  cos02pilt1  25111  cosne0  25114  recosf1o  25119  resinf1o  25120  efif1olem4  25129  logimul  25197  logcnlem3  25227  logf1o2  25233  ang180lem2  25388  heron  25416  acoscos  25471  emcllem7  25579  fsumharmonic  25589  ftalem2  25651  basellem1  25658  basellem2  25659  basellem3  25660  basellem5  25662  bposlem1  25860  bposlem2  25861  bposlem3  25862  lgsdirprm  25907  chebbnd1lem1  26045  chebbnd1lem2  26046  chebbnd1lem3  26047  mulog2sumlem2  26111  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2  26167  pntlemc  26171  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemr  26178  ostth2lem2  26210  ostth2lem3  26211  ostth2lem4  26212  ostth3  26214  axsegconlem3  26705  clwlkclwwlk2  27781  siilem1  28628  minvecolem2  28652  minvecolem4  28657  minvecolem5  28658  minvecolem6  28659  nmopcoi  29872  staddi  30023  cycpmco2lem4  30771  cycpmco2lem5  30772  hgt750lemd  31919  climlec3  32965  logi  32966  poimirlem26  34933  ftc1anclem8  34989  cntotbnd  35089  dalemply  36805  dalemsly  36806  dalem5  36818  dalem13  36827  dalem17  36831  dalem55  36878  dalem57  36880  lhpat3  37197  cdleme22aa  37490  jm2.27c  39653  hashnzfz2  40702  supxrubd  41429  suprnmpt  41479  fzisoeu  41616  upbdrech  41621  recnnltrp  41694  uzublem  41753  fmul01  41910  limsupubuzlem  42042  limsupequzmptlem  42058  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  stoweidlem36  42370  stoweidlem41  42375  wallispi2  42407  dirkercncflem1  42437  fourierdlem6  42447  fourierdlem7  42448  fourierdlem19  42460  fourierdlem20  42461  fourierdlem24  42465  fourierdlem25  42466  fourierdlem26  42467  fourierdlem30  42471  fourierdlem31  42472  fourierdlem42  42483  fourierdlem47  42487  fourierdlem48  42488  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem71  42511  fourierdlem79  42519  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fouriersw  42565  etransclem28  42596  etransclem48  42616  hoidmv1lelem1  42922  hoidmv1lelem3  42924  hoidmvlelem1  42926  hoidmvlelem4  42929  bgoldbtbndlem2  44020  lincresunit3lem2  44584  lincresunit3  44585  resum2sqgt0  44743  amgmwlem  44952