![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon2ai | Structured version Visualization version Unicode version |
Description: Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
Ref | Expression |
---|---|
necon2ai.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
necon2ai |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2ai.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con2i 124 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | neqned 2633 |
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 |
This theorem depends on definitions: df-bi 189 df-ne 2626 |
This theorem is referenced by: necon2i 2660 intex 4562 iin0 4580 opelopabsb 4714 0ellim 5488 inf3lem3 8140 cardmin2 8437 pm54.43 8439 canthp1lem2 9083 renepnf 9693 renemnf 9694 lt0ne0d 10186 nnne0 10649 hashnemnf 12534 hashnn0n0nn 12577 geolim 13938 geolim2 13939 georeclim 13940 geoisumr 13946 geoisum1c 13948 ramtcl2 14978 ramtcl2OLD 14979 lhop1 22978 logdmn0 23597 logcnlem3 23601 rusgranumwlkl1 25687 vcoprne 26210 strlem1 27915 subfacp1lem1 29914 rankeq1o 30950 poimirlem9 31961 poimirlem18 31970 poimirlem19 31971 poimirlem20 31972 poimirlem32 31984 fouriersw 38105 afvvfveq 38660 nn0nepnf 39089 |
Copyright terms: Public domain | W3C validator |