1    assume (p => q) & (-p => r) & (s => -r) & (s =>
     -q).
2      assume s.
3        (p => q) & (-p => r) & (s => -r).                 &E1 1
4        s => -q.                                          &E2 1
5        (p => q) & (-p => r).                             &E1 3
6        s => -r.                                          &E2 3
7        p => q.                                           &E1 5
8        -p => r.                                          &E2 5
9        assume p.
10         -q.                                             =>E 4,2
11         q.                                              =>E 7,9
12         F.                                              =>E 10,11
13       therefore -p.                                     =>I 9,12
14       r.                                                =>E 8,13
15       -r.                                               =>E 6,2
16       F.                                                =>E 15,14
17       t.                                                Efq 16
18     therefore s => t.                                   =>I 2,17
19   therefore (p => q) & (-p => r) & (s => -r) &
     (s => -q) => s => t.                                  =>I 1,18