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