Metamath Proof Explorer

Theorem notbid

Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994)

Ref Expression
Hypothesis notbid.1 
|- ( ph -> ( ps <-> ch ) )
Assertion notbid 
|- ( ph -> ( -. ps <-> -. ch ) )

Proof

Step Hyp Ref Expression
1 notbid.1 
 |-  ( ph -> ( ps <-> ch ) )
2 notnotb 
 |-  ( ps <-> -. -. ps )
3 notnotb 
 |-  ( ch <-> -. -. ch )
4 1 2 3 3bitr3g 
 |-  ( ph -> ( -. -. ps <-> -. -. ch ) )
5 4 con4bid 
 |-  ( ph -> ( -. ps <-> -. ch ) )