\and真值表：A \and \true \iff A
theorem wff_and_true_iff_self (A: wff): $ A \and \true \iff A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\neg (A \imp \neg \true) \iff \neg \neg A) \imp (\neg \neg A \iff A) \imp (\neg (A \imp \neg \true) \iff A) |
|
| 2 | iff_intro_neg | (A \imp \neg \true \iff \neg A) \imp (\neg (A \imp \neg \true) \iff \neg \neg A) |
|
| 3 | wff_imp_false_iff_neg_wff | A \imp \false \iff \neg A |
|
| 4 | 3 | conv false | A \imp \neg \true \iff \neg A |
| 5 | 2, 4 | ax_mp | \neg (A \imp \neg \true) \iff \neg \neg A |
| 6 | 1, 5 | ax_mp | (\neg \neg A \iff A) \imp (\neg (A \imp \neg \true) \iff A) |
| 7 | iff_symm | (A \iff \neg \neg A) \imp (\neg \neg A \iff A) |
|
| 8 | negneg_alloc | A \iff \neg \neg A |
|
| 9 | 7, 8 | ax_mp | \neg \neg A \iff A |
| 10 | 6, 9 | ax_mp | \neg (A \imp \neg \true) \iff A |
| 11 | 10 | conv and | A \and \true \iff A |