Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon4ad | Structured version Visualization version Unicode version |
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
Ref | Expression |
---|---|
necon4ad.1 |
Ref | Expression |
---|---|
necon4ad |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot 136 | . 2 | |
2 | necon4ad.1 | . . 3 | |
3 | 2 | necon1bd 2812 | . 2 |
4 | 1, 3 | syl5 34 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wceq 1483 wne 2794 |
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 197 df-ne 2795 |
This theorem is referenced by: necon1d 2816 fisseneq 8171 f1finf1o 8187 dfac5 8951 isf32lem9 9183 fpwwe2 9465 qextlt 12034 qextle 12035 xsubge0 12091 hashf1 13241 climuni 14283 rpnnen2lem12 14954 fzo0dvdseq 15045 4sqlem11 15659 haust1 21156 deg1lt0 23851 ply1divmo 23895 ig1peu 23931 dgrlt 24022 quotcan 24064 fta 24806 atcv0eq 29238 erdszelem9 31181 poimirlem23 33432 poimir 33442 lshpdisj 34274 lsatcv0eq 34334 exatleN 34690 atcvr0eq 34712 cdlemg31c 35987 jm2.19 37560 jm2.26lem3 37568 dgraa0p 37719 |
Copyright terms: Public domain | W3C validator |