Metamath Proof Explorer


Theorem xorneg2

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 xorneg2
|- ( ( ph \/_ -. ps ) <-> -. ( ph \/_ ps ) )

Proof

Step Hyp Ref Expression
1 df-xor
 |-  ( ( ph \/_ -. ps ) <-> -. ( ph <-> -. ps ) )
2 pm5.18
 |-  ( ( ph <-> ps ) <-> -. ( ph <-> -. ps ) )
3 xnor
 |-  ( ( ph <-> ps ) <-> -. ( ph \/_ ps ) )
4 1 2 3 3bitr2i
 |-  ( ( ph \/_ -. ps ) <-> -. ( ph \/_ ps ) )