Metamath Proof Explorer

Theorem necon2abid

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

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

Proof

Step Hyp Ref Expression
1 necon2abid.1 
 |-  ( ph -> ( A = B <-> -. ps ) )
2 notnotb 
 |-  ( ps <-> -. -. ps )
3 1 necon3abid 
 |-  ( ph -> ( A =/= B <-> -. -. ps ) )
4 2 3 bitr4id 
 |-  ( ph -> ( ps <-> A =/= B ) )