v6

|- A→(¬B→¬(A→B))

Důkaz

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