Theorem breqtrrdi 5184

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

Syntax hints:   → wi 4   = wceq 1534   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143

This theorem is referenced by:  enpr2d  9065  enpr2dOLD  9066  pw2eng  9094  undjudom  10182  dju1en  10186  djucomen  10192  djuassen  10193  xpdjuen  10194  infdjuabs  10221  ackbij1lem9  10243  unsnen  10568  1nqenq  10977  gtndiv  12661  xov1plusxeqvd  13499  intfrac2  13847  serle  14046  discr1  14225  faclbnd4lem1  14276  01sqrexlem1  15213  01sqrexlem4  15216  01sqrexlem7  15219  supcvg  15826  ege2le3  16058  eirrlem  16172  ruclem12  16209  bitsfzo  16401  pcprendvds  16800  pcpremul  16803  pcfaclem  16858  infpnlem2  16871  yonedainv  18264  srgbinomlem4  20160  lmcn2  23540  hmph0  23686  icccmplem2  24726  reconnlem2  24730  xrge0tsms  24737  minveclem2  25341  minveclem3b  25343  minveclem4  25347  minveclem6  25349  ivthlem2  25368  ivthlem3  25369  vitalilem2  25525  itg2seq  25659  itg2monolem1  25667  itg2monolem2  25668  itg2monolem3  25669  dveflem  25898  dvferm1lem  25903  dvferm2lem  25905  c1liplem1  25916  lhop1lem  25933  dvcvx  25940  plyeq0lem  26131  radcnvcl  26340  radcnvle  26343  psercnlem1  26349  psercn  26350  pilem3  26377  tangtx  26427  cos02pilt1  26447  cosne0  26450  recosf1o  26456  resinf1o  26457  efif1olem4  26466  logi  26508  logimul  26535  logcnlem3  26565  logf1o2  26571  ang180lem2  26729  heron  26757  acoscos  26812  emcllem7  26921  fsumharmonic  26931  ftalem2  26993  basellem1  27000  basellem2  27001  basellem3  27002  basellem5  27004  bposlem1  27204  bposlem2  27205  bposlem3  27206  lgsdirprm  27251  chebbnd1lem1  27389  chebbnd1lem2  27390  chebbnd1lem3  27391  mulog2sumlem2  27455  pntpbnd1a  27505  pntpbnd1  27506  pntpbnd2  27507  pntibndlem2  27511  pntlemc  27515  pntlemb  27517  pntlemg  27518  pntlemh  27519  pntlemr  27522  ostth2lem2  27554  ostth2lem3  27555  ostth2lem4  27556  ostth3  27558  axsegconlem3  28717  clwlkclwwlk2  29800  siilem1  30648  minvecolem2  30672  minvecolem4  30677  minvecolem5  30678  minvecolem6  30679  nmopcoi  31892  staddi  32043  cycpmco2lem4  32828  cycpmco2lem5  32829  hgt750lemd  34216  climlec3  35264  poimirlem26  37054  ftc1anclem8  37108  cntotbnd  37204  dalemply  39064  dalemsly  39065  dalem5  39077  dalem13  39086  dalem17  39090  dalem55  39137  dalem57  39139  lhpat3  39456  cdleme22aa  39749  aks4d1p1p7  41482  evlselv  41742  jm2.27c  42350  hashnzfz2  43681  supxrubd  44402  suprnmpt  44470  fzisoeu  44605  upbdrech  44610  recnnltrp  44682  uzublem  44735  fmul01  44891  limsupubuzlem  45023  limsupequzmptlem  45039  ioodvbdlimc1lem2  45243  ioodvbdlimc2lem  45245  stoweidlem36  45347  stoweidlem41  45352  wallispi2  45384  dirkercncflem1  45414  fourierdlem6  45424  fourierdlem7  45425  fourierdlem19  45437  fourierdlem20  45438  fourierdlem24  45442  fourierdlem25  45443  fourierdlem26  45444  fourierdlem30  45448  fourierdlem31  45449  fourierdlem42  45460  fourierdlem47  45464  fourierdlem48  45465  fourierdlem63  45480  fourierdlem64  45481  fourierdlem65  45482  fourierdlem71  45488  fourierdlem79  45496  fourierdlem89  45506  fourierdlem90  45507  fourierdlem91  45508  fouriersw  45542  etransclem28  45573  etransclem48  45593  hoidmv1lelem1  45902  hoidmv1lelem3  45904  hoidmvlelem1  45906  hoidmvlelem4  45909  bgoldbtbndlem2  47069  lincresunit3lem2  47471  lincresunit3  47472  resum2sqgt0  47703  amgmwlem  48158