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

Theorem syl6breqr 4079
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 2300 . 2  |-  B  =  C
41, 3syl6breq 4078 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  pw2eng  6984  cda1en  7817  ackbij1lem9  7870  unsnen  8191  1nqenq  8602  gtndiv  10105  xov1plusxeqvd  10796  intfrac2  10978  serle  11117  discr1  11253  faclbnd4lem1  11322  sqrlem1  11744  sqrlem4  11747  sqrlem7  11750  supcvg  12330  ege2le3  12387  eirrlem  12498  ruclem12  12535  bitsfzo  12642  pcprendvds  12909  pcpremul  12912  pcfaclem  12962  infpnlem2  12974  yonedainv  14071  lmcn2  17359  hmph0  17502  icccmplem2  18344  reconnlem2  18348  xrge0tsms  18355  minveclem2  18806  minveclem3b  18808  minveclem4  18812  minveclem6  18814  ivthlem2  18828  ivthlem3  18829  vitalilem2  18980  itg2seq  19113  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  dveflem  19342  dvferm1lem  19347  dvferm2lem  19349  c1liplem1  19359  lhop1lem  19376  dvcvx  19383  plyeq0lem  19608  radcnvcl  19809  radcnvle  19812  psercnlem1  19817  psercn  19818  pilem3  19845  tangtx  19889  cosne0  19908  recosf1o  19913  resinf1o  19914  efif1olem4  19923  logimul  19984  logcnlem3  20007  logf1o2  20013  ang180lem2  20124  acoscos  20205  emcllem7  20311  fsumharmonic  20321  ftalem2  20327  basellem1  20334  basellem2  20335  basellem3  20336  basellem5  20338  bposlem1  20539  bposlem2  20540  bposlem3  20541  lgsdirprm  20584  chebbnd1lem1  20634  chebbnd1lem2  20635  chebbnd1lem3  20636  mulog2sumlem2  20700  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntibndlem2  20756  pntlemc  20760  pntlemb  20762  pntlemg  20763  pntlemh  20764  pntlemr  20767  ostth2lem2  20799  ostth2lem3  20800  ostth2lem4  20801  ostth3  20803  siilem1  21445  minvecolem2  21470  minvecolem4  21475  minvecolem5  21476  minvecolem6  21477  nmopcoi  22691  staddi  22842  eupares  23914  eupap1  23915  axsegconlem3  24619  cntotbnd  26623  jm2.27c  27203  fmul01  27813  stoweidlem36  27888  stoweidlem41  27893  dalemply  30465  dalemsly  30466  dalem5  30478  dalem13  30487  dalem17  30491  dalem55  30538  dalem57  30540  lhpat3  30857  cdleme22aa  31150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator