Description: The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006) (Proof shortened by Wolf Lammen, 28-Jan-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nbn2 | |- ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm5.501 | |- ( -. ph -> ( -. ps <-> ( -. ph <-> -. ps ) ) ) |
|
| 2 | notbi | |- ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) ) |
|
| 3 | 1 2 | bitr4di | |- ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) ) |