Theorem true_and_false_iff_false ≪ | index | src | ≫

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

theorem true_and_false_iff_false: $ \true \and \false \iff \false $;

Step	Hyp	Ref	Expression
1		provneg_iff_false	\neg (\true \and \neg \true) \imp (\true \and \neg \true \iff \false)
2		contradiction	\neg (\true \and \neg \true)
3	1, 2	ax_mp	\true \and \neg \true \iff \false
4	3	conv false	\true \and \false \iff \false

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)