\and交换
theorem and_comm (A B: wff): $ A \and B \iff B \and A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_intro_neg | (A \imp \neg B \iff B \imp \neg A) \imp (\neg (A \imp \neg B) \iff \neg (B \imp \neg A)) |
|
| 2 | imp_neg_perm | A \imp \neg B \iff B \imp \neg A |
|
| 3 | 1, 2 | ax_mp | \neg (A \imp \neg B) \iff \neg (B \imp \neg A) |
| 4 | 3 | conv and | A \and B \iff B \and A |