This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ ⊻ ¬ ψ ↔ ¬ φ ⊻ ψ

Proof

Step Hyp Ref Expression
1 df-xor ⊢ φ ⊻ ¬ ψ ↔ ¬ φ ↔ ¬ ψ
2 pm5.18 ⊢ φ ↔ ψ ↔ ¬ φ ↔ ¬ ψ
3 xnor ⊢ φ ↔ ψ ↔ ¬ φ ⊻ ψ
4 1 2 3 3bitr2i ⊢ φ ⊻ ¬ ψ ↔ ¬ φ ⊻ ψ