NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nne Unicode version

Theorem nne 2520
Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.)
Assertion
Ref Expression
nne

Proof of Theorem nne
StepHypRef Expression
1 df-ne 2518 . . 3
21con2bii 322 . 2
32bicomi 193 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wb 176   wceq 1642   wne 2516
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 177  df-ne 2518
This theorem is referenced by:  neirr  2521  necon3ad  2552  necon3bd  2553  necon3ai  2556  necon3bi  2557  necon1bi  2559  necon2ai  2561  necon2ad  2564  necon4ai  2575  necon4i  2576  necon4ad  2577  necon4bd  2578  necon4d  2579  necon4bid  2582  necon1bd  2584  necon1d  2585  pm2.61ne  2591  pm2.61ine  2592  pm2.61dne  2593  ne3anior  2602  sbcne12g  3154  xpeq0  5046  xpcan  5057  xpcan2  5058
  Copyright terms: Public domain W3C validator