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 φψ