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

Theorem sylbb 218
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 215 . 2 (𝜓𝜒)
41, 3sylbi 216 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  bitri  274  elabgtOLD  3658  ssdifim  4261  ralf0  4515  disjxiun  5146  poclOLD  5598  wefrc  5672  frsn  5765  ssrel  5784  ssrelOLD  5785  funiun  7156  funopsn  7157  ssfi  9198  enfii  9214  nneneq  9234  fissuni  9383  inf3lem2  9654  rankvalb  9822  djur  9944  xrrebnd  13182  xaddf  13238  elfznelfzob  13774  fsuppmapnn0ub  13996  hashinfxadd  14380  hashfun  14432  fz1f1o  15692  dvdszzq  16696  clatl  18503  sgrp2nmndlem5  18889  mat1dimelbas  22417  cfinfil  23841  dyadmax  25571  ausgrusgri  29053  nbupgrres  29249  usgredgsscusgredg  29345  1egrvtxdg0  29397  wlkp1lem7  29565  isch3  31123  nmopun  31896  2ndresdju  32516  cycpm2tr  32932  esumnul  33798  dya2iocnrect  34032  bnj849  34687  bnj1279  34780  cusgr3cyclex  34877  bj-0int  36711  onsucuni3  36977  wl-nfeqfb  37134  poimirlem27  37251  sticksstones20  41769  sucomisnotcard  43116  iunrelexp0  43274  frege129d  43335  clsk3nimkb  43612  gneispace  43706  eliuniin  44605  eliuniin2  44626  stoweidlem48  45574  fourierdlem42  45675  fourierdlem80  45712  eubrdm  46556  oddprmALTV  47164  alimp-no-surprise  48400
  Copyright terms: Public domain W3C validator