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

Theorem necon2ai 2688
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 2656 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1370  =/=wne 2648
This theorem is referenced by:  necon2i  2696  neneqadOLD  2762  intex  4565  iin0  4583  opelopabsb  4716  0ellim  4898  inf3lem3  7973  cardmin2  8305  pm54.43  8307  canthp1lem2  8957  renepnf  9568  renemnf  9569  lt0ne0d  10042  nnne0  10492  hashnemnf  12272  hashnn0n0nn  12311  geolim  13488  geolim2  13489  georeclim  13490  geoisumr  13496  geoisum1c  13498  ramtcl2  14230  lhop1  21886  logdmn0  22485  logcnlem3  22489  vcoprne  24426  strlem1  26123  subfacp1lem1  27523  rankeq1o  28665  afvvfveq  30931  rusgranumwlkl1  31436
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 2650
  Copyright terms: Public domain W3C validator