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

Theorem sylbb 209
 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 206 . 2 (𝜓𝜒)
41, 3sylbi 207 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  bitri  264  ssdifim  3895  disjxiun  4681  trint  4801  pocl  5071  wefrc  5137  frsn  5223  ssrel  5241  funiun  6452  funopsn  6453  fissuni  8312  inf3lem2  8564  rankvalb  8698  xrrebnd  12037  xaddf  12093  elfznelfzob  12614  fsuppmapnn0ub  12835  hashinfxadd  13212  hashfun  13262  fz1f1o  14485  clatl  17163  sgrp2nmndlem5  17463  mat1dimelbas  20325  cfinfil  21744  dyadmax  23412  ausgrusgri  26108  nbupgrres  26310  usgredgsscusgredg  26411  1egrvtxdg0  26463  wlkp1lem7  26632  wwlksnfi  26869  isch3  28226  nmopun  29001  esumnul  30238  dya2iocnrect  30471  bnj849  31121  bnj1279  31212  bj-0int  33180  onsucuni3  33345  wl-nfeqfb  33453  poimirlem27  33566  unitresl  34014  iunrelexp0  38311  frege129d  38372  clsk3nimkb  38655  gneispace  38749  eliuniin  39593  eliuniin2  39617  stoweidlem48  40583  fourierdlem42  40684  fourierdlem80  40721  oddprmALTV  41923  alimp-no-surprise  42855
 Copyright terms: Public domain W3C validator