![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neeq12i | Structured version Visualization version Unicode version |
Description: Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Ref | Expression |
---|---|
neeq1i.1 |
![]() ![]() ![]() ![]() |
neeq12i.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
neeq12i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1i.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | neeq12i.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1, 2 | eqeq12i 2465 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | necon3bii 2676 |
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 1669 ax-4 1682 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-cleq 2444 df-ne 2624 |
This theorem is referenced by: 3netr3g 2702 3netr4g 2703 oppchomfval 15619 oppcbas 15623 rescbas 15734 rescco 15737 rescabs 15738 odubas 16379 oppglem 17001 mgplem 17728 mgpress 17734 opprlem 17856 sralem 18400 srasca 18404 sravsca 18405 opsrbaslem 18701 zlmsca 19092 znbaslem 19109 thlbas 19259 thlle 19260 matsca 19440 tuslem 21282 setsmsbas 21490 setsmsds 21491 tngds 21656 ttgval 24905 ttglem 24906 cchhllem 24917 axlowdimlem6 24977 zlmds 28768 zlmtset 28769 hlhilslem 35509 zlmodzxzldeplem 40344 |
Copyright terms: Public domain | W3C validator |