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

Theorem sylbb1 225
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 216 . 2 (𝜓𝜑)
3 sylbb1.2 . 2 (𝜑𝜒)
42, 3sylib 206 1 (𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  moeq  3344  fsuppmapnn0fiubex  12605  rrxcph  22901  cnvbraval  28155  ballotlemfp1  29682  finixpnum  32363  fin2so  32365  matunitlindflem1  32374  clsf2  37243  ellimcabssub0  38484  sge0iunmpt  39111  icceuelpartlem  39774  nnsum4primesodd  40013  nnsum4primesoddALTV  40014  umgrislfupgr  40346  usgrislfuspgr  40412  1wlkp1lem8  40887  elwwlks2s3  41167  eupthp1  41382
  Copyright terms: Public domain W3C validator