Theorem neg_true_iff_false ≪ | index | src | ≫

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

theorem neg_true_iff_false: $ \neg \true \iff \false $;
StepHypRefExpression
1 iff_refl 
\neg \true \iff \neg \true
2 1 conv false 
\neg \true \iff \false

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)