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

Theorem sylbb 220
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 217 . 2 (𝜓𝜒)
41, 3sylbi 218 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  bitri  276  unitresl  868  ssdifim  4242  disjxiun  5059  pocl  5479  wefrc  5547  frsn  5637  ssrel  5655  funiun  6904  funopsn  6905  fissuni  8821  inf3lem2  9084  rankvalb  9218  djur  9340  xrrebnd  12554  xaddf  12610  elfznelfzob  13136  fsuppmapnn0ub  13356  hashinfxadd  13739  hashfun  13791  fz1f1o  15059  clatl  17718  sgrp2nmndlem5  18029  mat1dimelbas  20998  cfinfil  22419  dyadmax  24116  ausgrusgri  26869  nbupgrres  27062  usgredgsscusgredg  27157  1egrvtxdg0  27209  wlkp1lem7  27377  wwlksnfiOLD  27601  isch3  28934  nmopun  29707  dvdszzq  30446  cycpm2tr  30677  esumnul  31195  dya2iocnrect  31427  bnj849  32085  bnj1279  32176  cusgr3cyclex  32269  bj-0int  34276  onsucuni3  34519  wl-nfeqfb  34646  poimirlem27  34788  iunrelexp0  39914  frege129d  39975  clsk3nimkb  40257  gneispace  40351  eliuniin  41232  eliuniin2  41254  stoweidlem48  42201  fourierdlem42  42302  fourierdlem80  42339  eubrdm  43139  oddprmALTV  43686  alimp-no-surprise  44716
  Copyright terms: Public domain W3C validator