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

Theorem sylbb1 238
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 229 . 2 (𝜓𝜑)
3 sylbb1.2 . 2 (𝜑𝜒)
42, 3sylib 219 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  fsuppmapnn0fiubex  13348  rrxcph  23922  volun  24073  umgrislfupgr  26835  usgrislfuspgr  26896  wlkp1lem8  27389  elwwlks2s3  27657  eupthp1  27922  cnvbraval  29814  ballotlemfp1  31648  finixpnum  34758  fin2so  34760  matunitlindflem1  34769  clsf2  40354  ellimcabssub0  41774  sge0iunmpt  42577  icceuelpartlem  43472  nnsum4primesodd  43838  nnsum4primesoddALTV  43839
  Copyright terms: Public domain W3C validator