A ⊃ ¬ ¬ A {\displaystyle A\supset \neg \neg A}
A ⊢ ¬ ¬ A {\displaystyle A\vdash \neg \neg A}
1. A ⊢ ( ¬ ¬ ¬ A ⊃ A ) ⊃ ( ( ¬ ¬ ¬ A ⊃ ¬ A ) ⊃ ¬ ¬ A ) {\displaystyle 1.\,\,A\vdash \left({\neg \neg \neg A\supset A}\right)\supset \left({\left({\neg \neg \neg A\supset \neg A}\right)\supset \neg \neg A}\right)}
// աքսիոմ 3 ( A = ¬ ¬ A , B = A {\displaystyle A=\neg \neg A,\,\,B=A} )
2. A ⊢ A {\displaystyle 2.\,\,A\vdash A}
// նախադրյալ
3. A ⊢ A ⊃ ( ¬ ¬ ¬ A ⊃ A ) {\displaystyle 3.\,\,A\vdash A\supset \left({\neg \neg \neg A\supset A}\right)}
// աքսիոմ 1 ( A = A , B = ¬ ¬ ¬ A {\displaystyle A=A,\,\,B=\neg \neg \neg A} )
4. A ⊢ ¬ ¬ ¬ A ⊃ A {\displaystyle 4.\,\,A\vdash \neg \neg \neg A\supset A}
// m.p. (2,3)
5. A ⊢ ( ¬ ¬ ¬ A ⊃ ¬ A ) ⊃ ¬ ¬ A {\displaystyle 5.\,\,A\vdash \left({\neg \neg \neg A\supset \neg A}\right)\supset \neg \neg A}
// m.p. (4,1)
6. A ⊢ ¬ ¬ ¬ A ⊃ ¬ A {\displaystyle 6.\,\,A\vdash \neg \neg \neg A\supset \neg A}
// բանաձև 1 ( A = ¬ A {\displaystyle A=\neg A} )
7. A ⊢ ¬ ¬ A {\displaystyle 7.\,\,A\vdash \neg \neg A}
// m.p. (6,5)
8. A ⊢ A ⊃ ¬ ¬ A {\displaystyle 8.\,\,A\vdash A\supset \neg \neg A}
// դեդուկցիայի թեորեմը