Metamath Proof Explorer

Theorem necon4abid

Description: Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008) (Proof shortened by Wolf Lammen, 24-Nov-2019)

Ref Expression
Hypothesis necon4abid.1 
|- ( ph -> ( A =/= B <-> -. ps ) )
Assertion necon4abid 
|- ( ph -> ( A = B <-> ps ) )

Proof

Step Hyp Ref Expression
1 necon4abid.1 
 |-  ( ph -> ( A =/= B <-> -. ps ) )
2 notnotb 
 |-  ( ps <-> -. -. ps )
3 1 necon1bbid 
 |-  ( ph -> ( -. -. ps <-> A = B ) )
4 2 3 bitr2id 
 |-  ( ph -> ( A = B <-> ps ) )