![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neeq1i | Structured version Visualization version Unicode version |
Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
Ref | Expression |
---|---|
neeq1i.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
neeq1i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1i.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | eqeq1i 2458 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | necon3bii 2678 |
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 1671 ax-4 1684 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-cleq 2446 df-ne 2626 |
This theorem is referenced by: eqnetri 2696 rabn0 3754 exss 4666 inisegn0 5203 suppvalbr 6923 brwitnlem 7214 en3lplem2 8125 hta 8373 kmlem3 8587 domtriomlem 8877 zorn2lem6 8936 konigthlem 8998 rpnnen1lem1 11297 rpnnen1lem2 11298 rpnnen1lem3 11299 rpnnen1lem5 11301 fsuppmapnn0fiubex 12211 seqf1olem1 12259 iscyg2 17529 gsumval3lem2 17552 opprirred 17942 ptclsg 20642 iscusp2 21329 dchrptlem1 24204 dchrptlem2 24205 disjex 28214 disjexc 28215 signsply0 29452 signstfveq0a 29477 bnj1177 29827 bnj1253 29838 fin2so 31944 stoweidlem36 37907 aovnuoveq 38703 aovovn0oveq 38706 ovn0dmfun 39868 aacllem 40644 |
Copyright terms: Public domain | W3C validator |