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 ( ( 𝜑𝜓 ) → ¬ ( 𝜑𝜓 ) )