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