\neg\imp布尔等价式
theorem negimp_boole_def (A B: wff): $ \neg (A \imp B) \iff A \and \neg B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_intro_neg | (A \imp B \iff A \imp \neg \neg B) \imp (\neg (A \imp B) \iff \neg (A \imp \neg \neg B)) |
|
| 2 | iff_introl_imp | (B \iff \neg \neg B) \imp (A \imp B \iff A \imp \neg \neg B) |
|
| 3 | negneg_alloc | B \iff \neg \neg B |
|
| 4 | 2, 3 | ax_mp | A \imp B \iff A \imp \neg \neg B |
| 5 | 1, 4 | ax_mp | \neg (A \imp B) \iff \neg (A \imp \neg \neg B) |
| 6 | 5 | conv and | \neg (A \imp B) \iff A \and \neg B |