Description: Move negation outside of biconditional. Compare Theorem *5.18 of WhiteheadRussell p. 124. (Contributed by NM, 27-Jun-2002) (Proof shortened by Wolf Lammen, 20-Sep-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nbbn | |- ( ( -. ph <-> ps ) <-> -. ( ph <-> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xor3 | |- ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) ) |
|
| 2 | con2bi | |- ( ( ph <-> -. ps ) <-> ( ps <-> -. ph ) ) |
|
| 3 | bicom | |- ( ( ps <-> -. ph ) <-> ( -. ph <-> ps ) ) |
|
| 4 | 1 2 3 | 3bitrri | |- ( ( -. ph <-> ps ) <-> -. ( ph <-> ps ) ) |