1    p v ~p
 2    (p & ~p) -> q
 3    (p & ~p) -> (q v ~q)
 4    (p & (p -> q)) -> q
 5    p -> (q -> p)
 6    p -> (q -> q)
 7    p -> (p -> p)
 8    (p -> ~p) -> ~p
 9    (t -> p) -> p    equivalently    ((p -> p) -> q) -> q
 10   p -> (t -> p)
 11   p v (p -> q)
 12   T ->. F -> F
 13   (q -> p) -> ((p -> q) -> (p -> r))
 14   (p -> q) -> ((q -> r) -> (p -> r))
 15   p -> ((p -> q) -> q)
 16   (p -> (p -> q)) -> (p -> q)
 17   (p -> (q -> r)) -> (q -> (p -> r))
 18   ((p -> q) & (q -> r)) -> (p -> r)


.