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

Theorem sylbb 197
Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.)
Hypotheses
Ref Expression
sylbb.1  |-  ( ph  <->  ps )
sylbb.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
sylbb  |-  ( ph  ->  ch )

Proof of Theorem sylbb
StepHypRef Expression
1 sylbb.1 . 2  |-  ( ph  <->  ps )
2 sylbb.2 . . 3  |-  ( ps  <->  ch )
32biimpi 194 . 2  |-  ( ps 
->  ch )
41, 3sylbi 195 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  bitri  249  trint  4548  pocl  4800  wefrc  4866  fissuni  7814  inf3lem2  8035  rankvalb  8204  xrrebnd  11358  xaddf  11412  elfznelfzob  11873  fsuppmapnn0ub  12057  hashinfxadd  12408  hashfun  12448  wrdeqswrdlsw  12624  clatl  15592  mat1dimelbas  18733  cfinfil  20122  dyadmax  21735  wwlknfi  24400  isch3  25821  nmopun  26595  esumnul  27685  dya2iocnrect  27878  wl-nfeqfb  29553  unitresl  30072  stoweidlem48  31303  alimp-no-surprise  32152  bnj849  32937  bnj1279  33028
  Copyright terms: Public domain W3C validator