\and归一
theorem and_unify (A: wff): $ A \and A \iff A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | (\neg (A \imp \neg A) \imp A) \imp (A \imp \neg (A \imp \neg A)) \imp (\neg (A \imp \neg A) \iff A) |
|
| 2 | neg_imp_swap | (\neg A \imp A \imp \neg A) \imp \neg (A \imp \neg A) \imp A |
|
| 3 | introl_imp | \neg A \imp A \imp \neg A |
|
| 4 | 2, 3 | ax_mp | \neg (A \imp \neg A) \imp A |
| 5 | 1, 4 | ax_mp | (A \imp \neg (A \imp \neg A)) \imp (\neg (A \imp \neg A) \iff A) |
| 6 | imp_neg_swap | ((A \imp \neg A) \imp \neg A) \imp A \imp \neg (A \imp \neg A) |
|
| 7 | imp_neg_tosame_neg | (A \imp \neg A) \imp \neg A |
|
| 8 | 6, 7 | ax_mp | A \imp \neg (A \imp \neg A) |
| 9 | 5, 8 | ax_mp | \neg (A \imp \neg A) \iff A |
| 10 | 9 | conv and | A \and A \iff A |