Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon2ai Unicode version

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
StepHypRef Expression
1 necon2ai.1 . . 3
21con2i 120 . 2
32neqned 2660 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator