ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylbb GIF version

Theorem sylbb 122
Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.)
Hypotheses
Ref Expression
sylbb.1 (𝜑𝜓)
sylbb.2 (𝜓𝜒)
Assertion
Ref Expression
sylbb (𝜑𝜒)

Proof of Theorem sylbb
StepHypRef Expression
1 sylbb.1 . 2 (𝜑𝜓)
2 sylbb.2 . . 3 (𝜓𝜒)
32biimpi 119 . 2 (𝜓𝜒)
41, 3sylbi 120 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ctinfom  12376
  Copyright terms: Public domain W3C validator