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