Theorem necon2ai 2692

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

Assertion

Ref	Expression
necon2ai

Proof of Theorem necon2ai

Step	Hyp	Ref	Expression
1		necon2ai.1	. . 3
2	1	con2i 120	. 2
3	2	neqned 2660	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652

This theorem is referenced by:  necon2i  2700  neneqadOLD  2766  intex  4608  iin0  4626  opelopabsb  4762  0ellim  4945  inf3lem3  8068  cardmin2  8400  pm54.43  8402  canthp1lem2  9052  renepnf  9662  renemnf  9663  lt0ne0d  10143  nnne0  10593  hashnemnf  12417  hashnn0n0nn  12458  geolim  13679  geolim2  13680  georeclim  13681  geoisumr  13687  geoisum1c  13689  ramtcl2  14529  lhop1  22415  logdmn0  23021  logcnlem3  23025  rusgranumwlkl1  24947  vcoprne  25472  strlem1  27169  subfacp1lem1  28623  rankeq1o  29828  fouriersw  32014  afvvfveq  32233

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 2654