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