Theorem necon2ai 2683

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	neneqad 2652	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1370   =/= wne 2644

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 2646

This theorem is referenced by:  necon2i  2691  neneqadOLD  2757  intex  4548  iin0  4566  opelopabsb  4699  0ellim  4881  inf3lem3  7939  cardmin2  8271  pm54.43  8273  canthp1lem2  8923  renepnf  9534  renemnf  9535  lt0ne0d  10008  nnne0  10457  hashnemnf  12218  hashnn0n0nn  12257  geolim  13434  geolim2  13435  georeclim  13436  geoisumr  13442  geoisum1c  13444  ramtcl2  14176  lhop1  21604  logdmn0  22203  logcnlem3  22207  vcoprne  24094  strlem1  25791  subfacp1lem1  27203  rankeq1o  28345  afvvfveq  30194  rusgranumwlkl1  30699