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

Theorem sylbb1 240
 Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)
Hypotheses
Ref Expression
sylbb1.1 (𝜑𝜓)
sylbb1.2 (𝜑𝜒)
Assertion
Ref Expression
sylbb1 (𝜓𝜒)

Proof of Theorem sylbb1
StepHypRef Expression
1 sylbb1.1 . . 3 (𝜑𝜓)
21biimpri 231 . 2 (𝜓𝜑)
3 sylbb1.2 . 2 (𝜑𝜒)
42, 3sylib 221 1 (𝜓𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  fsuppmapnn0fiubex  13357  rrxcph  24003  volun  24156  umgrislfupgr  26923  usgrislfuspgr  26984  wlkp1lem8  27477  elwwlks2s3  27744  eupthp1  28008  cnvbraval  29900  ballotlemfp1  31871  finixpnum  35058  fin2so  35060  matunitlindflem1  35069  clsf2  40844  ellimcabssub0  42274  sge0iunmpt  43072  icceuelpartlem  43967  nnsum4primesodd  44329  nnsum4primesoddALTV  44330
 Copyright terms: Public domain W3C validator