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  3515  fsuppmapnn0fiubex  12978  rrxcph  23372  umgrislfupgr  26209  usgrislfuspgr  26270  wlkp1lem8  26779  elwwlks2s3  27063  eupthp1  27360  cnvbraval  29270  ballotlemfp1  30854  finixpnum  33699  fin2so  33701  matunitlindflem1  33710  clsf2  38918  ellimcabssub0  40344  sge0iunmpt  41130  icceuelpartlem  41873  nnsum4primesodd  42186  nnsum4primesoddALTV  42187
 Copyright terms: Public domain W3C validator