\imp布尔等价式
theorem imp_boole_def (A B: wff): $ A \imp B \iff \neg A \or B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_intror_imp | (A \iff \neg \neg A) \imp (A \imp B \iff \neg \neg A \imp B) |
|
| 2 | negneg_alloc | A \iff \neg \neg A |
|
| 3 | 1, 2 | ax_mp | A \imp B \iff \neg \neg A \imp B |
| 4 | 3 | conv or | A \imp B \iff \neg A \or B |