Description: Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 22-Nov-2019)

|- ( A =/= B -> -. ph )

|- ( ph -> A = B )

|- ( ph -> -. -. ph )

|- ( -. -. ph -> A = B )