Theorem necon2ai 2695

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

Hypothesis

Ref	Expression
necon2ai.1	|- ( A = B -> -. ph )

Assertion

Ref	Expression
necon2ai	|- ( ph -> A =/= B )

Proof of Theorem necon2ai

Step	Hyp	Ref	Expression
1		necon2ai.1	. . 3 |- ( A = B -> -. ph )
2	1	con2i 120	. 2 |- ( ph -> -. A = B )
3	2	neqned 2663	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1374   =/= wne 2655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-ne 2657

This theorem is referenced by:  necon2i  2703  neneqadOLD  2769  intex  4596  iin0  4614  opelopabsb  4750  0ellim  4933  inf3lem3  8036  cardmin2  8368  pm54.43  8370  canthp1lem2  9020  renepnf  9630  renemnf  9631  lt0ne0d  10107  nnne0  10557  hashnemnf  12372  hashnn0n0nn  12413  geolim  13631  geolim2  13632  georeclim  13633  geoisumr  13639  geoisum1c  13641  ramtcl2  14377  lhop1  22143  logdmn0  22742  logcnlem3  22746  rusgranumwlkl1  24609  vcoprne  25134  strlem1  26831  subfacp1lem1  28249  rankeq1o  29391  afvvfveq  31655