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 ¬ φ
Assertion notatnand ¬ φ ψ

Proof

Step Hyp Ref Expression
1 notatnand.1 ¬ φ
2 1 intnanr ¬ φ ψ