Metamath Proof Explorer

Theorem 2falsed

Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013) (Proof shortened by Wolf Lammen, 11-Apr-2024)

Ref Expression
Hypotheses 2falsed.1 
|- ( ph -> -. ps )
2falsed.2 
|- ( ph -> -. ch )
Assertion 2falsed 
|- ( ph -> ( ps <-> ch ) )

Proof

Step Hyp Ref Expression
1 2falsed.1 
 |-  ( ph -> -. ps )
2 2falsed.2 
 |-  ( ph -> -. ch )
3 1 2 2thd 
 |-  ( ph -> ( -. ps <-> -. ch ) )
4 3 con4bid 
 |-  ( ph -> ( ps <-> ch ) )