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  874  elabgt  3596  ssdifim  4193  ralf0  4441  disjxiun  5067  poclOLD  5502  wefrc  5574  frsn  5665  ssrel  5683  funiun  7001  funopsn  7002  ssfi  8918  enfii  8932  fissuni  9054  inf3lem2  9317  rankvalb  9486  djur  9608  xrrebnd  12831  xaddf  12887  elfznelfzob  13421  fsuppmapnn0ub  13643  hashinfxadd  14028  hashfun  14080  fz1f1o  15350  clatl  18141  sgrp2nmndlem5  18483  mat1dimelbas  21528  cfinfil  22952  dyadmax  24667  ausgrusgri  27441  nbupgrres  27634  usgredgsscusgredg  27729  1egrvtxdg0  27781  wlkp1lem7  27949  isch3  29504  nmopun  30277  2ndresdju  30887  dvdszzq  31031  cycpm2tr  31288  esumnul  31916  dya2iocnrect  32148  bnj849  32805  bnj1279  32898  cusgr3cyclex  32998  bj-0int  35199  onsucuni3  35465  wl-nfeqfb  35622  poimirlem27  35731  sticksstones20  40050  iunrelexp0  41199  frege129d  41260  clsk3nimkb  41539  gneispace  41633  eliuniin  42538  eliuniin2  42558  stoweidlem48  43479  fourierdlem42  43580  fourierdlem80  43617  eubrdm  44417  oddprmALTV  45027  alimp-no-surprise  46371
  Copyright terms: Public domain W3C validator