MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6breqr Structured version   Unicode version

Theorem syl6breqr 4320
Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
syl6breqr.1  |-  ( ph  ->  A R B )
syl6breqr.2  |-  C  =  B
Assertion
Ref Expression
syl6breqr  |-  ( ph  ->  A R C )

Proof of Theorem syl6breqr
StepHypRef Expression
1 syl6breqr.1 . 2  |-  ( ph  ->  A R B )
2 syl6breqr.2 . . 3  |-  C  =  B
32eqcomi 2437 . 2  |-  B  =  C
41, 3syl6breq 4319 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  pw2eng  7405  cda1en  8332  ackbij1lem9  8385  unsnen  8705  1nqenq  9119  gtndiv  10707  xov1plusxeqvd  11418  intfrac2  11681  serle  11845  discr1  11984  faclbnd4lem1  12053  sqrlem1  12716  sqrlem4  12719  sqrlem7  12722  supcvg  13301  ege2le3  13358  eirrlem  13469  ruclem12  13506  bitsfzo  13614  pcprendvds  13890  pcpremul  13893  pcfaclem  13943  infpnlem2  13955  yonedainv  15074  lmcn2  19064  hmph0  19210  icccmplem2  20242  reconnlem2  20246  xrge0tsms  20253  minveclem2  20755  minveclem3b  20757  minveclem4  20761  minveclem6  20763  ivthlem2  20778  ivthlem3  20779  vitalilem2  20931  itg2seq  21062  itg2monolem1  21070  itg2monolem2  21071  itg2monolem3  21072  dveflem  21293  dvferm1lem  21298  dvferm2lem  21300  c1liplem1  21310  lhop1lem  21327  dvcvx  21334  plyeq0lem  21563  radcnvcl  21767  radcnvle  21770  psercnlem1  21775  psercn  21776  pilem3  21803  tangtx  21852  cosne0  21871  recosf1o  21876  resinf1o  21877  efif1olem4  21886  logimul  21948  logcnlem3  21974  logf1o2  21980  ang180lem2  22091  heron  22118  acoscos  22173  emcllem7  22280  fsumharmonic  22290  ftalem2  22296  basellem1  22303  basellem2  22304  basellem3  22305  basellem5  22307  bposlem1  22508  bposlem2  22509  bposlem3  22510  lgsdirprm  22553  chebbnd1lem1  22603  chebbnd1lem2  22604  chebbnd1lem3  22605  mulog2sumlem2  22669  pntpbnd1a  22719  pntpbnd1  22720  pntpbnd2  22721  pntibndlem2  22725  pntlemc  22729  pntlemb  22731  pntlemg  22732  pntlemh  22733  pntlemr  22736  ostth2lem2  22768  ostth2lem3  22769  ostth2lem4  22770  ostth3  22772  axsegconlem3  22988  eupares  23419  eupap1  23420  siilem1  24074  minvecolem2  24099  minvecolem4  24104  minvecolem5  24105  minvecolem6  24106  nmopcoi  25322  staddi  25473  climlec3  27248  ftc1anclem8  28318  cntotbnd  28539  jm2.27c  29201  fmul01  29606  stoweidlem36  29677  stoweidlem41  29682  wallispi2  29714  clwlkisclwwlk2  30298  lincresunit3lem2  30744  lincresunit3  30745  dalemply  32892  dalemsly  32893  dalem5  32905  dalem13  32914  dalem17  32918  dalem55  32965  dalem57  32967  lhpat3  33284  cdleme22aa  33577
  Copyright terms: Public domain W3C validator