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

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

Proof of Theorem sylbb
StepHypRef Expression
1 sylbb.1 . 2
2 sylbb.2 . . 3
32biimpi 194 . 2
41, 3sylbi 195 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184 This theorem is referenced by:  bitri  249  trint  4560  pocl  4812  wefrc  4878  fissuni  7845  inf3lem2  8067  rankvalb  8236  xrrebnd  11398  xaddf  11452  elfznelfzob  11916  fsuppmapnn0ub  12101  hashinfxadd  12453  hashfun  12495  wrdeqswrdlsw  12674  clatl  15746  sgrp2nmndlem5  16047  mat1dimelbas  18973  cfinfil  20394  dyadmax  22007  wwlknfi  24738  isch3  26159  nmopun  26933  esumnul  28059  dya2iocnrect  28252  wl-nfeqfb  29990  unitresl  30482  stoweidlem48  31830  fourierdlem42  31931  fourierdlem80  31969  alimp-no-surprise  33196  bnj849  33983  bnj1279  34074  rp-isfinite6  37744  frege70  37961 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
 Copyright terms: Public domain W3C validator