p → q →. p → ~q → ~p

(a)  [p →. q → ~.p → p] →. p → q →. p → ~.p → p
     Regla 2, Axioma 2

(b)  [~q →. q → ~.p → p] →. p → ~q →. p →. q → ~.p → p
     Regla 2, transitividad de →

(c)  ~q →. q → ~.p → p
     Regla 2, ex falso sequitur quodlibet
(d)  p → ~q →. p →. q → ~.p → p
     Regla 1, b y c

(e)  p → ~q →. p → q →. p → ~.p → p
     Lema 3, d y a

(f)  p → ~[p → p] → ~p →. [p → q →. p → ~[p → p]] →. p → q →. ~p
     Regla 2, transitividad de →

g  [~p →. p → p] →. ~[p → p] → ~~p
    Modus tollens

h  ~[p → p] → ~~p
     Regla 1, g y ex falso sequitud quodlibet

i   ~~p → p →. ~[p → p] → ~~p →. ~[p → p] → p
    transitividad de →

j   ~[p → p] → p
    Regla 1, i y Doble negación, y Regla 1, h.

k   p → ~[p → p] → p
     Lema 1, j


l  [p → q →. p → ~[p → p]] →. p → q → ~p
     Regla 1,  f y k

m  p → ~q →. p → q →. ~p
     Lema 3, e y l

p →. ~q → ~[p → q]

Una prueba de  p →. ~q → ~[p → q]
 

(a) p → q → q →. ~q → ~[p → q]
    Sust., Modus tollens

(c) p → q →. p → q
    Sust., reflexividad de →

(d) p → q → p →. p → q → q
    Lema 2, (c)

(f) p →. p → q → p →. p → q → q
    Modus ponens, (d)

(g) [p →. p → q → p] →. p →. p → q → q
    Lema 2, (f)

(h) p →. p → q → p
    Sust., Axioma 1

(i) p →. p → q → q
    Modus ponens, (g y h)

(j) p →. q → ~[p → q]
    Lema 3, (a e i)