Metamath Proof Explorer


Theorem nbn2

Description: The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006) (Proof shortened by Wolf Lammen, 28-Jan-2013)

Ref Expression
Assertion nbn2 ¬ φ ¬ ψ φ ψ

Proof

Step Hyp Ref Expression
1 pm5.501 ¬ φ ¬ ψ ¬ φ ¬ ψ
2 notbi φ ψ ¬ φ ¬ ψ
3 1 2 bitr4di ¬ φ ¬ ψ φ ψ