\or真值表：wff \or \false \iff wff
theorem wff_or_false_iff_wff (A: wff): $ A \or \false \iff A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\neg A \imp \neg \true \iff \true \imp A) \imp (\true \imp A \iff A) \imp (\neg A \imp \neg \true \iff A) |
|
| 2 | iff_symm | (\true \imp A \iff \neg A \imp \neg \true) \imp (\neg A \imp \neg \true \iff \true \imp A) |
|
| 3 | imp_allocrev_neg | \true \imp A \iff \neg A \imp \neg \true |
|
| 4 | 2, 3 | ax_mp | \neg A \imp \neg \true \iff \true \imp A |
| 5 | 1, 4 | ax_mp | (\true \imp A \iff A) \imp (\neg A \imp \neg \true \iff A) |
| 6 | trueimp_eqv_self | \true \imp A \iff A |
|
| 7 | 5, 6 | ax_mp | \neg A \imp \neg \true \iff A |
| 8 | 7 | conv false, or | A \or \false \iff A |