Syllogism is a tautology by kiritex

module Theorem where

  open import Definitions
  open import Data.Bool

  syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
  syllogism-is-tauto P Q R φ with ev P φ | ev Q φ | ev R φ
  ... | true | true | true = refl
  ... | true | true | false = refl
  ... | true | false | _ = refl
  ... | false | true | true = refl
  ... | false | true | false = refl
  ... | false | false | true = refl
  ... | false | false | false = refl