\iff指配\neg
theorem iff_alloc_neg (A B: wff): $ (A \iff B) \iff \neg A \iff \neg B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | ((A \iff B) \imp (\neg A \iff \neg B)) \imp ((\neg A \iff \neg B) \imp (A \iff B)) \imp ((A \iff B) \iff \neg A \iff \neg B) |
|
| 2 | iff_intro_neg | (A \iff B) \imp (\neg A \iff \neg B) |
|
| 3 | 1, 2 | ax_mp | ((\neg A \iff \neg B) \imp (A \iff B)) \imp ((A \iff B) \iff \neg A \iff \neg B) |
| 4 | neg_iff_elim | (\neg A \iff \neg B) \imp (A \iff B) |
|
| 5 | 3, 4 | ax_mp | (A \iff B) \iff \neg A \iff \neg B |