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

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

Proof of Theorem nne
StepHypRef Expression
1 df-ne 2518 . . 3 (AB ↔ ¬ A = B)
21con2bii 322 . 2 (A = B ↔ ¬ AB)
32bicomi 193 1 ABA = B)
 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