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

Theorem necon2ai 2672
 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 124 . 2
32neqned 2650 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wceq 1452   wne 2641 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 190  df-ne 2643 This theorem is referenced by:  necon2i  2677  intex  4557  iin0  4575  opelopabsb  4711  0ellim  5492  inf3lem3  8153  cardmin2  8450  pm54.43  8452  canthp1lem2  9096  renepnf  9706  renemnf  9707  lt0ne0d  10200  nnne0  10664  hashnemnf  12565  hashnn0n0nn  12608  geolim  14003  geolim2  14004  georeclim  14005  geoisumr  14011  geoisum1c  14013  ramtcl2  15045  ramtcl2OLD  15046  lhop1  23045  logdmn0  23664  logcnlem3  23668  rusgranumwlkl1  25754  vcoprne  26279  strlem1  27984  subfacp1lem1  29974  rankeq1o  31009  poimirlem9  32013  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem32  32036  fouriersw  38207  afvvfveq  38795  nn0nepnf  39229
 Copyright terms: Public domain W3C validator