Description: The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 3-Oct-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nbn.1 | |- -. ph |
|
| Assertion | nbn | |- ( -. ps <-> ( ps <-> ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nbn.1 | |- -. ph |
|
| 2 | bibif | |- ( -. ph -> ( ( ps <-> ph ) <-> -. ps ) ) |
|
| 3 | 1 2 | ax-mp | |- ( ( ps <-> ph ) <-> -. ps ) |
| 4 | 3 | bicomi | |- ( -. ps <-> ( ps <-> ph ) ) |