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 ) )