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  4503  pocl  4750  wefrc  4816  fissuni  7779  inf3lem2  7999  rankvalb  8167  xrrebnd  11340  xaddf  11394  elfznelfzob  11866  fsuppmapnn0ub  12055  hashinfxadd  12408  hashfun  12451  clatl  15962  sgrp2nmndlem5  16263  mat1dimelbas  19157  cfinfil  20578  dyadmax  22191  wwlknfi  25036  isch3  26453  nmopun  27226  esumnul  28375  dya2iocnrect  28609  bnj849  29191  bnj1279  29282  wl-nfeqfb  31343  unitresl  31745  rp-isfinite6  35591  iunrelexp0  35662  frege129d  35723  stoweidlem48  37180  fourierdlem42  37281  fourierdlem80  37319  icceuelpartlem  37682  oddprmALTV  37749  alimp-no-surprise  38820
  Copyright terms: Public domain W3C validator