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