Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nne | Structured version Visualization version Unicode version |
Description: Negation of inequality. (Contributed by NM, 9-Jun-2006.) |
Ref | Expression |
---|---|
nne |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2795 | . . 3 | |
2 | 1 | con2bii 347 | . 2 |
3 | 2 | bicomi 214 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wb 196 wceq 1483 wne 2794 |
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 197 df-ne 2795 |
This theorem is referenced by: neirr 2803 necon3bd 2808 necon1d 2816 necon4d 2818 necon3ai 2819 necon4bid 2839 necon1bbii 2843 pm2.61ine 2877 pm2.61dne 2880 ne3anior 2887 sbcne12 3986 raldifsnb 4325 tpprceq3 4335 tppreqb 4336 prneimg 4388 prnebg 4389 xpeq0 5554 xpcan 5570 xpcan2 5571 funtpgOLD 5943 fndmdifeq0 6323 ftpg 6423 fnnfpeq0 6444 suppimacnv 7306 fnsuppres 7322 ixp0 7941 isfin5-2 9213 zornn0g 9327 nn0n0n1ge2b 11359 fsuppmapnn0fiub0 12793 fsuppmapnn0ub 12795 mptnn0fsupp 12797 mptnn0fsuppr 12799 discr 13001 hashgt12el 13210 hashgt12el2 13211 hashtpg 13267 fprodle 14727 alzdvds 15042 algcvgblem 15290 lcmfunsnlem2lem2 15352 lssne0 18951 dsmm0cl 20084 pmatcollpw2lem 20582 elcls 20877 cmpfi 21211 bwth 21213 1stccnp 21265 dissnlocfin 21332 trfil3 21692 isufil2 21712 bcth3 23128 rrxmvallem 23187 mdegleb 23824 tglowdim1i 25396 tglineintmo 25537 lmieu 25676 uvtxa01vtx 26298 uhgrvd00 26430 wlkon2n0 26562 wwlks 26727 rusgrnumwwlks 26869 1to2vfriswmgr 27143 numclwwlk3lem 27241 frgrregord013 27253 nmlno0lem 27648 lnon0 27653 nmlnop0iALT 28854 atom1d 29212 uniinn0 29366 funcnv5mpt 29469 xaddeq0 29518 bnj521 30805 bnj1533 30922 bnj1541 30926 bnj1279 31086 bnj1280 31088 bnj1311 31092 nepss 31599 poimirlem31 33440 poimirlem32 33441 itg2addnclem2 33462 ftc1anc 33493 n0elqs 34098 lfl1 34357 lkreqN 34457 pmap0 35051 paddasslem17 35122 ltrnnid 35422 ntrneikb 38392 fzdifsuc2 39525 limclr 39887 fourierdlem42 40366 fourierdlem76 40399 sge0cl 40598 meadjiunlem 40682 oddprmne2 41624 mndpsuppss 42152 islininds2 42273 |
Copyright terms: Public domain | W3C validator |