¬A→(A→B)
Vezmu formuli |- ¬A→(¬B→¬A)
to je instance A1, použiju na první negované A větu o dedukci, dostanu
¬A |- ¬B→¬A
Dále vezmu A3 - (¬B→¬A)→(A→B) a pravidlem modus ponens
¬B->¬A (¬B->¬A)->(A->B) ------------------------------- A->B
dostanu
¬A |- A→B
Potom už stačí jednou použít větu o dedukci
|- ¬A→(A→B)
a tvrzení v2 je dokázáno (teda snad)
QED