![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon1bd | Structured version Visualization version Unicode version |
Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
Ref | Expression |
---|---|
necon1bd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
necon1bd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2635 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | necon1bd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5bir 226 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con1d 129 |
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 190 df-ne 2635 |
This theorem is referenced by: necon4ad 2655 fvclss 6172 suppssr 6973 eceqoveq 7494 fofinf1o 7878 cantnfp1lem3 8211 cantnfp1 8212 mul0or 10280 inelr 10627 rimul 10628 rlimuni 13663 pc2dvds 14877 divsfval 15502 pleval2i 16259 lssvs0or 18382 lspsnat 18417 lmmo 20445 filssufilg 20975 hausflimi 21044 fclscf 21089 xrsmopn 21879 rectbntr0 21899 bcth3 22348 limcco 22897 ig1pdvds 23177 ig1pdvdsOLD 23183 plyco0 23195 plypf1 23215 coeeulem 23227 coeidlem 23240 coeid3 23243 coemullem 23253 coemulhi 23257 coemulc 23258 dgradd2 23271 vieta1lem2 23313 dvtaylp 23374 musum 24169 perfectlem2 24207 dchrelbas3 24215 dchrmulid2 24229 dchreq 24235 dchrsum 24246 dchrisum0re 24400 coltr 24741 lmieu 24875 elspansn5 27276 atomli 28084 onsucconi 31146 poimirlem8 31993 poimirlem9 31994 poimirlem18 32003 poimirlem21 32006 poimirlem22 32007 poimirlem26 32011 lshpcmp 32599 lsator0sp 32612 atnle 32928 atlatmstc 32930 osumcllem8N 33573 osumcllem11N 33576 pexmidlem5N 33584 pexmidlem8N 33587 dochsat0 35070 dochexmidlem5 35077 dochexmidlem8 35080 congabseq 35869 perfectALTVlem2 38882 |
Copyright terms: Public domain | W3C validator |