Theorem necon2ai 2660

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 124	. 2 |- ( ph -> -. A = B )
3	2	neqned 2628	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1438   =/= wne 2619

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 189  df-ne 2621

This theorem is referenced by:  necon2i  2668  neneqadOLD  2734  intex  4578  iin0  4596  opelopabsb  4728  0ellim  5502  inf3lem3  8139  cardmin2  8435  pm54.43  8437  canthp1lem2  9080  renepnf  9690  renemnf  9691  lt0ne0d  10181  nnne0  10644  hashnemnf  12528  hashnn0n0nn  12571  geolim  13919  geolim2  13920  georeclim  13921  geoisumr  13927  geoisum1c  13929  ramtcl2  14959  ramtcl2OLD  14960  lhop1  22958  logdmn0  23577  logcnlem3  23581  rusgranumwlkl1  25667  vcoprne  26190  strlem1  27895  subfacp1lem1  29904  rankeq1o  30937  poimirlem9  31907  poimirlem18  31916  poimirlem19  31917  poimirlem20  31918  poimirlem32  31930  fouriersw  37959  afvvfveq  38406