|- A→(¬B→¬(A→B))
Vyjdu z dlouhými léty prověřené implikace
|- (A→B)→(A→B)
(mj. to platí podle v1)
Dvěma použitími věty o dedukci dojdu k
A, A→B |- B
A znova, tentokrát obráceným směrem
A |- (A→B)→B
Dle v5 a modus ponens
(A->B)->B [(A->B)->B]->[¬B->¬(A->B)] ------------------------------------------ ¬B->¬(A->B)
A |- ¬B→¬(A→B)
A ještě jednou věta o dedukci
|- A→[¬B→¬(A→B)]
QED