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

Theorem sylbb 208
 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 205 . 2 (𝜓𝜒)
41, 3sylbi 206 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  bitri  263  disjxiun  4579  trint  4696  pocl  4966  wefrc  5032  frsn  5112  ssrel  5130  funiun  6318  funopsn  6319  fissuni  8154  inf3lem2  8409  rankvalb  8543  xrrebnd  11873  xaddf  11929  elfznelfzob  12440  fsuppmapnn0ub  12657  hashinfxadd  13035  hashfun  13084  clatl  16939  sgrp2nmndlem5  17239  mat1dimelbas  20096  cfinfil  21507  dyadmax  23172  wwlknfi  26266  isch3  27482  nmopun  28257  esumnul  29437  dya2iocnrect  29670  bnj849  30249  bnj1279  30340  onsucuni3  32391  wl-nfeqfb  32502  poimirlem27  32606  unitresl  33054  iunrelexp0  37013  frege129d  37074  clsk3nimkb  37358  gneispace  37452  stoweidlem48  38941  fourierdlem42  39042  fourierdlem80  39079  oddprmALTV  40136  ausgrusgri  40398  nbupgrres  40592  usgredgsscusgredg  40675  1egrvtxdg0  40727  1wlkp1lem7  40888  wwlksnfi  41112  alimp-no-surprise  42336
 Copyright terms: Public domain W3C validator