Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon2abid | Structured version Visualization version Unicode version |
Description: Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.) |
Ref | Expression |
---|---|
necon2abid.1 |
Ref | Expression |
---|---|
necon2abid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon2abid.1 | . . 3 | |
2 | 1 | necon3abid 2830 | . 2 |
3 | notnotb 304 | . 2 | |
4 | 2, 3 | syl6rbbr 279 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 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: sossfld 5580 fin23lem24 9144 isf32lem4 9178 sqgt0sr 9927 leltne 10127 xrleltne 11978 xrltne 11994 ge0nemnf 12004 xlt2add 12090 supxrbnd 12158 supxrre2 12161 ioopnfsup 12663 icopnfsup 12664 xblpnfps 22200 xblpnf 22201 nmoreltpnf 27624 nmopreltpnf 28728 funeldmb 31661 elprneb 41296 |
Copyright terms: Public domain | W3C validator |