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

Theorem sylbb1 236
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 227 . 2 (𝜓𝜑)
3 sylbb1.2 . 2 (𝜑𝜒)
42, 3sylib 217 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:  fsuppmapnn0fiubex  13957  rrxcph  24909  volun  25062  umgrislfupgr  28383  usgrislfuspgr  28444  wlkp1lem8  28937  elwwlks2s3  29205  eupthp1  29469  cnvbraval  31363  ballotlemfp1  33490  finixpnum  36473  fin2so  36475  matunitlindflem1  36484  oeord2com  42061  clsf2  42877  ellimcabssub0  44333  sge0iunmpt  45134  icceuelpartlem  46103  nnsum4primesodd  46464  nnsum4primesoddALTV  46465
  Copyright terms: Public domain W3C validator