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 ( 𝜑𝜓 )