![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neeq2 | Structured version Visualization version Unicode version |
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.) |
Ref | Expression |
---|---|
neeq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | neeq2d 2695 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-cleq 2454 df-ne 2634 |
This theorem is referenced by: psseq2 3532 fprg 6096 f1dom3el3dif 6193 f1prex 6206 dfac5 8584 kmlem4 8608 kmlem14 8618 1re 9667 hashge2el2difr 12670 dvdsle 14398 sgrp2rid2ex 16709 isirred 17975 isnzr2 18535 dmatelnd 19569 mdetdiaglem 19671 mdetunilem1 19685 mdetunilem2 19686 maducoeval2 19713 hausnei 20392 regr1lem2 20803 xrhmeo 22022 axtg5seg 24561 axtgupdim2 24567 axtgeucl 24568 ishlg 24695 tglnpt2 24734 axlowdim1 25037 2pthoncl 25381 clwlknclwlkdifs 25736 3cyclfrgrarn1 25788 4cycl2vnunb 25793 numclwwlk2lem1 25878 numclwlk2lem2f 25879 superpos 28055 signswch 29498 axtgupdim2OLD 29533 dfrdg4 30766 fvray 30956 linedegen 30958 fvline 30959 linethru 30968 hilbert1.1 30969 poimirlem1 31985 hlsuprexch 32990 3dim1lem5 33075 llni2 33121 lplni2 33146 2llnjN 33176 lvoli2 33190 2lplnj 33229 islinei 33349 cdleme40n 34079 cdlemg33b 34318 ax6e2ndeq 36969 ax6e2ndeqVD 37345 ax6e2ndeqALT 37367 refsum2cnlem1 37397 stoweidlem43 37941 nnfoctbdjlem 38330 elprneb 38749 structgrssvtxlem 39170 2pthdlem1 39878 3pthdlem1 39904 upgr3v3e3cycl 39920 upgr4cycl4dv4e 39925 usgvad2edg 39995 |
Copyright terms: Public domain | W3C validator |