\or真值表：\false \or \true \iff \true
theorem false_or_true_iff_true: $ \false \or \true \iff \true $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\false \or \true \iff \true \or \false) \imp (\true \or \false \iff \true) \imp (\false \or \true \iff \true) |
|
| 2 | or_comm | \false \or \true \iff \true \or \false |
|
| 3 | 1, 2 | ax_mp | (\true \or \false \iff \true) \imp (\false \or \true \iff \true) |
| 4 | true_or_false_iff_true | \true \or \false \iff \true |
|
| 5 | 3, 4 | ax_mp | \false \or \true \iff \true |