Metamath Proof Explorer

Theorem xornan

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

Ref Expression
Assertion xornan 
|- ( ( ph \/_ ps ) -> -. ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 xor2 
 |-  ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
2 1 simprbi 
 |-  ( ( ph \/_ ps ) -> -. ( ph /\ ps ) )