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  unitreslOLD  876  elabgt  3624  ssdifim  4222  ralf0  4471  disjxiun  5102  poclOLD  5553  wefrc  5627  frsn  5719  ssrel  5738  ssrelOLD  5739  funiun  7092  funopsn  7093  ssfi  9116  enfii  9132  nneneq  9152  fissuni  9300  inf3lem2  9564  rankvalb  9732  djur  9854  xrrebnd  13086  xaddf  13142  elfznelfzob  13677  fsuppmapnn0ub  13899  hashinfxadd  14284  hashfun  14336  fz1f1o  15594  clatl  18396  sgrp2nmndlem5  18738  mat1dimelbas  21818  cfinfil  23242  dyadmax  24960  ausgrusgri  28066  nbupgrres  28259  usgredgsscusgredg  28354  1egrvtxdg0  28406  wlkp1lem7  28574  isch3  30130  nmopun  30903  2ndresdju  31512  dvdszzq  31655  cycpm2tr  31912  esumnul  32587  dya2iocnrect  32821  bnj849  33477  bnj1279  33570  cusgr3cyclex  33670  bj-0int  35562  onsucuni3  35828  wl-nfeqfb  35985  poimirlem27  36095  sticksstones20  40564  sucomisnotcard  41797  iunrelexp0  41955  frege129d  42016  clsk3nimkb  42293  gneispace  42387  eliuniin  43290  eliuniin2  43311  stoweidlem48  44260  fourierdlem42  44361  fourierdlem80  44398  eubrdm  45241  oddprmALTV  45850  alimp-no-surprise  47199
  Copyright terms: Public domain W3C validator