\iff真值表：(\true \iff A) \iff A
theorem true_iff_wff_iff_wff (A: wff): $ (\true \iff A) \iff A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | ((\true \iff A) \iff A \iff \true) \imp ((A \iff \true) \iff A) \imp ((\true \iff A) \iff A) |
|
| 2 | iff_comm | (\true \iff A) \iff A \iff \true |
|
| 3 | 1, 2 | ax_mp | ((A \iff \true) \iff A) \imp ((\true \iff A) \iff A) |
| 4 | wff_iff_true_iff_self | (A \iff \true) \iff A |
|
| 5 | 3, 4 | ax_mp | (\true \iff A) \iff A |