Theorem negfalse_proof ≪ | index | src | ≫

\neg\false证明

theorem negfalse_proof: $ \neg \false $;
StepHypRefExpression
1 negneg_intro 
\true \imp \neg \neg \true
2 true_proof 
\true
3 1, 2 ax_mp 
\neg \neg \true
4 3 conv false 
\neg \false

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)