假值合成
theorem false_comp (A: wff): $ A \imp \neg A \imp \false $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_imp_swapl | (\neg A \imp A \imp \false) \imp A \imp \neg A \imp \false |
|
| 2 | imp_tran | (\neg A \imp (A \iff \false)) \imp ((A \iff \false) \imp A \imp \false) \imp \neg A \imp A \imp \false |
|
| 3 | provneg_iff_false | \neg A \imp (A \iff \false) |
|
| 4 | 2, 3 | ax_mp | ((A \iff \false) \imp A \imp \false) \imp \neg A \imp A \imp \false |
| 5 | iff_decomp | (A \iff \false) \imp A \imp \false |
|
| 6 | 4, 5 | ax_mp | \neg A \imp A \imp \false |
| 7 | 1, 6 | ax_mp | A \imp \neg A \imp \false |