Metamath Proof Explorer


Theorem 2false

Description: Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005) (Proof shortened by Wolf Lammen, 19-May-2013)

Ref Expression
Hypotheses 2false.1 ¬ φ
2false.2 ¬ ψ
Assertion 2false φ ψ

Proof

Step Hyp Ref Expression
1 2false.1 ¬ φ
2 2false.2 ¬ ψ
3 1 2 2th ¬ φ ¬ ψ
4 3 con4bii φ ψ