Metamath Proof Explorer

Theorem necon1abid

Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007) (Proof shortened by Wolf Lammen, 24-Nov-2019)

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

Proof

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