Description: The connector \/_ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 27-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xorneg1 | |- ( ( -. ph \/_ ps ) <-> -. ( ph \/_ ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xorcom | |- ( ( -. ph \/_ ps ) <-> ( ps \/_ -. ph ) ) |
|
| 2 | xorneg2 | |- ( ( ps \/_ -. ph ) <-> -. ( ps \/_ ph ) ) |
|
| 3 | xorcom | |- ( ( ps \/_ ph ) <-> ( ph \/_ ps ) ) |
|
| 4 | 2 3 | xchbinx | |- ( ( ps \/_ -. ph ) <-> -. ( ph \/_ ps ) ) |
| 5 | 1 4 | bitri | |- ( ( -. ph \/_ ps ) <-> -. ( ph \/_ ps ) ) |