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
|- -. ph
2false.2
|- -. ps
Assertion 2false
|- ( ph <-> ps )

Proof

Step Hyp Ref Expression
1 2false.1
 |-  -. ph
2 2false.2
 |-  -. ps
3 1 2 2th
 |-  ( -. ph <-> -. ps )
4 3 con4bii
 |-  ( ph <-> ps )