Description: Given falsum F. , we can define the negation of a wff ph as the statement that F. follows from assuming ph . (Contributed by Mario Carneiro, 9-Feb-2017) (Proof shortened by Wolf Lammen, 21-Jul-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfnot | |- ( -. ph <-> ( ph -> F. ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fal | |- -. F. |
|
| 2 | mtt | |- ( -. F. -> ( -. ph <-> ( ph -> F. ) ) ) |
|
| 3 | 1 2 | ax-mp | |- ( -. ph <-> ( ph -> F. ) ) |