MPE Home 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  3997  disjxiun  4793  trint  4912  pocl  5186  wefrc  5252  frsn  5338  ssrel  5356  funiun  6567  funopsn  6568  fissuni  8428  inf3lem2  8691  rankvalb  8825  djur  8941  xrrebnd  12184  xaddf  12240  elfznelfzob  12760  fsuppmapnn0ub  12981  hashinfxadd  13358  hashfun  13408  fz1f1o  14632  clatl  17309  sgrp2nmndlem5  17609  mat1dimelbas  20471  cfinfil  21890  dyadmax  23558  ausgrusgri  26254  nbupgrres  26456  usgredgsscusgredg  26557  1egrvtxdg0  26609  wlkp1lem7  26778  wwlksnfi  27016  isch3  28399  nmopun  29174  esumnul  30411  dya2iocnrect  30644  bnj849  31294  bnj1279  31385  bj-0int  33353  onsucuni3  33518  wl-nfeqfb  33628  poimirlem27  33741  unitresl  34189  iunrelexp0  38488  frege129d  38549  clsk3nimkb  38832  gneispace  38926  eliuniin  39770  eliuniin2  39794  stoweidlem48  40760  fourierdlem42  40861  fourierdlem80  40898  oddprmALTV  42100  alimp-no-surprise  43032
  Copyright terms: Public domain W3C validator