Theorem nne 2021

Description: Negation of inequality.

Assertion

Ref	Expression
nne	|- (-. A =/= B <-> A = B)

Proof of Theorem nne

Step	Hyp	Ref	Expression
1		df-ne 2019	. . 3 |- (A =/= B <-> -. A = B)
2	1	con2bii 238	. 2 |- (A = B <-> -. A =/= B)
3	2	bicomi 189	1 |- (-. A =/= B <-> A = B)

Syntax hints:  -. wn 2   <-> wb 163   = wceq 1298   =/= wne 2017

This theorem is referenced by:  necon3ad 2037  necon3bd 2039  necon3ai 2043  necon3bi 2045  necon1bi 2048  necon2ai 2051  necon2ad 2055  necon4ai 2067  necon4i 2069  necon4ad 2071  necon4bd 2073  necon4d 2075  necon4bid 2078  necon1bd 2080  necon1d 2082  pm2.61ne 2087  pm2.61ine 2089  pm2.61dne 2091  fr0 3636  xpeq0 4336  xpcan 4348  xpcan2 4350  1re 6598  elcls 8980  bcthlem7 9283  0ngrp 9335  nmlno0lem 9793  lnon0 9798  usinuniop 10341  nmlnop0iALT 11557  atom1d 11925  bnj521 12522  bnj1278 13035  bnj1305 13048  bnj1475 13152  bnj1533 13182  bnj1284 13482  alzdvds 13695  gcdeq0 13727  algcvgblem 13745  nepss 13820  negcmpprcal2 14276  bwt2 14960  alexsublem4 15440  locfincomp 15514  isufil2 15565  fcluscf 15612  flimfnfcls 15615  zornn0 15764  sbcne12g 16409  pmap0 17245  padd01 17272  padd02 17273  paddasslem17 17297

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-ne 2019

Copyright terms: Public domain