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

Theorem sylbb1 227
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 218 . 2 (𝜓𝜑)
3 sylbb1.2 . 2 (𝜑𝜒)
42, 3sylib 208 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  moeq  3380  fsuppmapnn0fiubex  12787  rrxcph  23174  umgrislfupgr  26012  usgrislfuspgr  26073  wlkp1lem8  26571  elwwlks2s3  26853  eupthp1  27069  cnvbraval  28953  ballotlemfp1  30538  finixpnum  33374  fin2so  33376  matunitlindflem1  33385  clsf2  38250  ellimcabssub0  39655  sge0iunmpt  40404  icceuelpartlem  41141  nnsum4primesodd  41455  nnsum4primesoddALTV  41456
  Copyright terms: Public domain W3C validator