\and真值表：\false \and A \iff \false
theorem false_and_wff_iff_false (A: wff): $ \false \and A \iff \false $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\false \and A \iff A \and \false) \imp (A \and \false \iff \false) \imp (\false \and A \iff \false) |
|
| 2 | and_comm | \false \and A \iff A \and \false |
|
| 3 | 1, 2 | ax_mp | (A \and \false \iff \false) \imp (\false \and A \iff \false) |
| 4 | wff_and_false_iff_false | A \and \false \iff \false |
|
| 5 | 3, 4 | ax_mp | \false \and A \iff \false |