\iff真值表：(\true \iff \false) \iff \false
theorem true_iff_false_iff_false: $ (\true \iff \false) \iff \false $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_symm | (\false \iff \true \iff \false) \imp ((\true \iff \false) \iff \false) |
|
| 2 | iff_tran | (\false \iff \false \iff \true) \imp ((\false \iff \true) \iff \true \iff \false) \imp (\false \iff \true \iff \false) |
|
| 3 | assgin_true | \false \iff \false \iff \true |
|
| 4 | 2, 3 | ax_mp | ((\false \iff \true) \iff \true \iff \false) \imp (\false \iff \true \iff \false) |
| 5 | iff_comm | (\false \iff \true) \iff \true \iff \false |
|
| 6 | 4, 5 | ax_mp | \false \iff \true \iff \false |
| 7 | 1, 6 | ax_mp | (\true \iff \false) \iff \false |