Metamath Proof Explorer

Theorem notatnand

Description: Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016)

Ref Expression
Hypothesis notatnand.1 
|- -. ph
Assertion notatnand 
|- -. ( ph /\ ps )

Proof

Step Hyp Ref Expression
1 notatnand.1 
 |-  -. ph
2 1 intnanr 
 |-  -. ( ph /\ ps )