Theorem neg_false_iff_true ≪ | index | src | ≫

\neg真值表：\neg \false \iff \true

theorem neg_false_iff_true: $ \neg \false \iff \true $;

Step	Hyp	Ref	Expression
1		iff_symm	(\true \iff \neg \neg \true) \imp (\neg \neg \true \iff \true)
2		negneg_alloc	\true \iff \neg \neg \true
3	1, 2	ax_mp	\neg \neg \true \iff \true
4	3	conv false	\neg \false \iff \true

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)