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  4509  pocl  4757  wefrc  4823  fissuni  7728  inf3lem2  7947  rankvalb  8116  xrrebnd  11252  xaddf  11306  elfznelfzob  11749  hashinfxadd  12267  hashfun  12318  wrdeqswrdlsw  12462  clatl  15406  cfinfil  19599  dyadmax  21212  isch3  24797  nmopun  25571  esumnul  26648  dya2iocnrect  26841  wl-nfeqfb  28515  unitresl  29034  stoweidlem48  29992  wwlknfi  30519  fsuppmapnn0ub  30945  mat1dimelbas  31034  alimp-no-surprise  31466  bnj849  32251  bnj1279  32342
  Copyright terms: Public domain W3C validator