Metamath Proof Explorer


Theorem nannot

Description: Negation in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007) (Revised by Wolf Lammen, 26-Jun-2020)

Ref Expression
Assertion nannot ¬φφφ

Proof

Step Hyp Ref Expression
1 dfnan2 φφφ¬φ
2 pm4.8 φ¬φ¬φ
3 1 2 bitr2i ¬φφφ