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

Metamath Proof Explorer

Theorem xornan

Description: Exclusive disjunction implies alternative denial ("XOR implies NAND"). (Contributed by BJ, 19-Apr-2019)

Ref Expression
Assertion xornan ⊢ φ ⊻ ψ → ¬ φ ∧ ψ

Proof

Step Hyp Ref Expression
1 xor2 ⊢ φ ⊻ ψ ↔ φ ∨ ψ ∧ ¬ φ ∧ ψ
2 1 simprbi ⊢ φ ⊻ ψ → ¬ φ ∧ ψ