否定的定理与\false等价
theorem provneg_iff_false (A: wff): $ \neg A \imp (A \iff \false) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_eliml | ((\true \iff \neg A) \iff A \iff \neg \true) \imp (\true \iff \neg A) \imp (A \iff \neg \true) |
|
| 2 | 1 | _hyp_null_complete | \neg A \imp ((\true \iff \neg A) \iff A \iff \neg \true) \imp (\true \iff \neg A) \imp (A \iff \neg \true) |
| 3 | iff_neg_perm | (\true \iff \neg A) \iff A \iff \neg \true |
|
| 4 | 3 | _hyp_null_complete | \neg A \imp ((\true \iff \neg A) \iff A \iff \neg \true) |
| 5 | 2, 4 | _hyp_mp | \neg A \imp (\true \iff \neg A) \imp (A \iff \neg \true) |
| 6 | iff_symm | (\neg A \iff \true) \imp (\true \iff \neg A) |
|
| 7 | 6 | _hyp_null_complete | \neg A \imp (\neg A \iff \true) \imp (\true \iff \neg A) |
| 8 | prov_iff_true | \neg A \imp (\neg A \iff \true) |
|
| 9 | 8 | _hyp_null_complete | \neg A \imp \neg A \imp (\neg A \iff \true) |
| 10 | _hyp_null_intro | \neg A \imp \neg A |
|
| 11 | 9, 10 | _hyp_mp | \neg A \imp (\neg A \iff \true) |
| 12 | 7, 11 | _hyp_mp | \neg A \imp (\true \iff \neg A) |
| 13 | 5, 12 | _hyp_mp | \neg A \imp (A \iff \neg \true) |
| 14 | 13 | conv false | \neg A \imp (A \iff \false) |