Theorem syl6breqr 4695

Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
syl6breqr.1	⊢ (𝜑 → 𝐴𝑅𝐵)
syl6breqr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
syl6breqr	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem syl6breqr

Step	Hyp	Ref	Expression
1		syl6breqr.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		syl6breqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2631	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6breq 4694	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  pw2eng  8066  cda1en  8997  ackbij1lem9  9050  unsnen  9375  1nqenq  9784  gtndiv  11454  xov1plusxeqvd  12318  intfrac2  12657  serle  12856  discr1  13000  faclbnd4lem1  13080  sqrlem1  13983  sqrlem4  13986  sqrlem7  13989  supcvg  14588  ege2le3  14820  eirrlem  14932  ruclem12  14970  bitsfzo  15157  pcprendvds  15545  pcpremul  15548  pcfaclem  15602  infpnlem2  15615  yonedainv  16921  srgbinomlem4  18543  lmcn2  21452  hmph0  21598  icccmplem2  22626  reconnlem2  22630  xrge0tsms  22637  minveclem2  23197  minveclem3b  23199  minveclem4  23203  minveclem6  23205  ivthlem2  23221  ivthlem3  23222  vitalilem2  23378  itg2seq  23509  itg2monolem1  23517  itg2monolem2  23518  itg2monolem3  23519  dveflem  23742  dvferm1lem  23747  dvferm2lem  23749  c1liplem1  23759  lhop1lem  23776  dvcvx  23783  plyeq0lem  23966  radcnvcl  24171  radcnvle  24174  psercnlem1  24179  psercn  24180  pilem3  24207  tangtx  24257  cosne0  24276  recosf1o  24281  resinf1o  24282  efif1olem4  24291  logimul  24360  logcnlem3  24390  logf1o2  24396  ang180lem2  24540  heron  24565  acoscos  24620  emcllem7  24728  fsumharmonic  24738  ftalem2  24800  basellem1  24807  basellem2  24808  basellem3  24809  basellem5  24811  bposlem1  25009  bposlem2  25010  bposlem3  25011  lgsdirprm  25056  chebbnd1lem1  25158  chebbnd1lem2  25159  chebbnd1lem3  25160  mulog2sumlem2  25224  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntlemc  25284  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemr  25291  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth3  25327  axsegconlem3  25799  clwlkclwwlk2  26904  siilem1  27706  minvecolem2  27731  minvecolem4  27736  minvecolem5  27737  minvecolem6  27738  nmopcoi  28954  staddi  29105  hgt750lemd  30726  climlec3  31619  logi  31620  poimirlem26  33435  ftc1anclem8  33492  cntotbnd  33595  dalemply  34940  dalemsly  34941  dalem5  34953  dalem13  34962  dalem17  34966  dalem55  35013  dalem57  35015  lhpat3  35332  cdleme22aa  35627  jm2.27c  37574  hashnzfz2  38520  supxrubd  39297  suprnmpt  39355  fzisoeu  39514  upbdrech  39519  recnnltrp  39593  uzublem  39657  fmul01  39812  limsupubuzlem  39944  limsupequzmptlem  39960  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem36  40253  stoweidlem41  40258  wallispi2  40290  dirkercncflem1  40320  fourierdlem6  40330  fourierdlem7  40331  fourierdlem19  40343  fourierdlem20  40344  fourierdlem24  40348  fourierdlem25  40349  fourierdlem26  40350  fourierdlem30  40354  fourierdlem31  40355  fourierdlem42  40366  fourierdlem47  40370  fourierdlem48  40371  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem71  40394  fourierdlem79  40402  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fouriersw  40448  etransclem28  40479  etransclem48  40499  hoidmv1lelem1  40805  hoidmv1lelem3  40807  hoidmvlelem1  40809  hoidmvlelem4  40812  bgoldbtbndlem2  41694  lincresunit3lem2  42269  lincresunit3  42270  amgmwlem  42548