Theorem false_iff_false_iff_true ≪ | index | src | ≫

\iff真值表：(\false \iff \false) \iff \true

theorem false_iff_false_iff_true: $ (\false \iff \false) \iff \true $;

Step	Hyp	Ref	Expression
1		prov_iff_true	(\false \iff \false) \imp ((\false \iff \false) \iff \true)
2		iff_refl	\false \iff \false
3	1, 2	ax_mp	(\false \iff \false) \iff \true

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)