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

Metamath Proof Explorer

Theorem xornan2

Description: XOR implies NAND (written with the -/\ connector). (Contributed by BJ, 19-Apr-2019)

Ref Expression
Assertion xornan2 ⊢ φ ⊻ ψ → φ ⊼ ψ

Proof

Step Hyp Ref Expression
1 xornan ⊢ φ ⊻ ψ → ¬ φ ∧ ψ
2 df-nan ⊢ φ ⊼ ψ ↔ ¬ φ ∧ ψ
3 1 2 sylibr ⊢ φ ⊻ ψ → φ ⊼ ψ