Theorem true_or_false_iff_true ≪ | index | src | ≫

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

theorem true_or_false_iff_true: $ \true \or \false \iff \true $;
StepHypRefExpression
1 prov_iff_true 
(\neg \true \imp \neg \true) \imp (\neg \true \imp \neg \true \iff \true)
2 imp_refl 
\neg \true \imp \neg \true
3 1, 2 ax_mp 
\neg \true \imp \neg \true \iff \true
4 3 conv false 
\neg \true \imp \false \iff \true
5 4 conv or 
\true \or \false \iff \true

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)