\neg\iff置换
theorem neg_iff_perm (A B: wff): $ (\neg A \iff B) \iff \neg B \iff A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_simintro_and | (\neg A \imp B \iff \neg B \imp A) \imp (B \imp \neg A \iff A \imp \neg B) \imp ((\neg A \imp B) \and (B \imp \neg A) \iff (\neg B \imp A) \and (A \imp \neg B)) |
|
| 2 | neg_imp_perm | \neg A \imp B \iff \neg B \imp A |
|
| 3 | 1, 2 | ax_mp | (B \imp \neg A \iff A \imp \neg B) \imp ((\neg A \imp B) \and (B \imp \neg A) \iff (\neg B \imp A) \and (A \imp \neg B)) |
| 4 | imp_neg_perm | B \imp \neg A \iff A \imp \neg B |
|
| 5 | 3, 4 | ax_mp | (\neg A \imp B) \and (B \imp \neg A) \iff (\neg B \imp A) \and (A \imp \neg B) |
| 6 | 5 | conv iff | (\neg A \iff B) \iff \neg B \iff A |