|- ¬¬A→A
Pro důkaz použiju tvrzení v2 ve tvaru
|- ¬¬A→(¬A→¬¬¬A)
Podle věty o dedukci
¬¬A |- ¬A→¬¬¬A
Dále s pomocí instance A3 (¬A→¬¬¬A)→(¬¬A→A) a modus ponens
¬A->¬¬¬A (¬A->¬¬¬A)->(¬¬A->A) ----------------------------------- ¬¬A->A
¬¬A |- ¬¬A→A
Opět použiju větu o dedukci
¬¬A |- A
a znova, tentokrát opačným směrem
|- ¬¬A → A
QED