# Syllogism is a tautology by nrolland

```module Theorem where

open import Definitions
open import Data.Bool renaming(true to t;false to f)

module NoStructure where
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 φ
... | t | t | t = refl
... | t | t | f = refl
... | t | f | t = refl
... | t | f | f = refl
... | f | t | t = refl
... | f | t | f = refl
... | f | f | t = refl
... | f | f | f = refl

module MixingEvAndTraversal where
syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
syllogism-is-tauto P Q R phi with ev P phi
syllogism-is-tauto P Q R phi | t with ev Q phi
syllogism-is-tauto P Q R phi | t | t with ev R phi
syllogism-is-tauto P Q R phi | t | t | t = refl
syllogism-is-tauto P Q R phi | t | t | f = refl
syllogism-is-tauto P Q R phi | t | f = refl
syllogism-is-tauto P Q R phi | f with ev Q phi
syllogism-is-tauto P Q R phi | f | t with ev R phi
syllogism-is-tauto P Q R phi | f | t | t = refl
syllogism-is-tauto P Q R phi | f | t | f = refl
syllogism-is-tauto P Q R phi | f | f = refl

module Kawai where
_⇒_ : Bool -> Bool -> Bool
a ⇒ b = not a ∨  b

syl : ∀ (p q r : Bool) -> ((p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r))) == t
syl t t t = refl
syl t t f = refl
syl t f r = refl
syl f t t = refl
syl f t f = refl
syl f f r = refl

syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
syllogism-is-tauto p q r c = syl (ev p c) (ev q c) (ev r c)

open Kawai public
```