Metamath Proof Explorer

Theorem xornan2

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

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

Proof

Step Hyp Ref Expression
1 xornan 
 |-  ( ( ph \/_ ps ) -> -. ( ph /\ ps ) )
2 df-nan 
 |-  ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )
3 1 2 sylibr 
 |-  ( ( ph \/_ ps ) -> ( ph -/\ ps ) )