Theorem nne 2521

Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.)

Assertion

Ref	Expression
nne	⊢ (¬ A ≠ B ↔ A = B)

Proof of Theorem nne

Step	Hyp	Ref	Expression
1		df-ne 2519	. . 3 ⊢ (A ≠ B ↔ ¬ A = B)
2	1	con2bii 322	. 2 ⊢ (A = B ↔ ¬ A ≠ B)
3	2	bicomi 193	1 ⊢ (¬ A ≠ B ↔ A = B)

Syntax hints:  ¬ wn 3   ↔ wb 176   = wceq 1642   ≠ wne 2517

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 2519

This theorem is referenced by:  neirr  2522  necon3ad  2553  necon3bd  2554  necon3ai  2557  necon3bi  2558  necon1bi  2560  necon2ai  2562  necon2ad  2565  necon4ai  2576  necon4i  2577  necon4ad  2578  necon4bd  2579  necon4d  2580  necon4bid  2583  necon1bd  2585  necon1d  2586  pm2.61ne  2592  pm2.61ine  2593  pm2.61dne  2594  ne3anior  2603  sbcne12g  3155  xpeq0  5047  xpcan  5058  xpcan2  5059