Metamath Proof Explorer

Theorem necon2bbid

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

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

Proof

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