Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon1bi | Structured version Visualization version Unicode version |
Description: Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
Ref | Expression |
---|---|
necon1bi.1 |
Ref | Expression |
---|---|
necon1bi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2795 | . . 3 | |
2 | necon1bi.1 | . . 3 | |
3 | 1, 2 | sylbir 225 | . 2 |
4 | 3 | con1i 144 | 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: necon4ai 2825 fvbr0 6215 peano5 7089 1stnpr 7172 2ndnpr 7173 1st2val 7194 2nd2val 7195 eceqoveq 7853 mapprc 7861 ixp0 7941 setind 8610 hashfun 13224 hashf1lem2 13240 iswrdi 13309 dvdsrval 18645 thlle 20041 konigsberg 27119 hatomistici 29221 esumrnmpt2 30130 mppsval 31469 setindtr 37591 fourierdlem72 40395 afvpcfv0 41226 |
Copyright terms: Public domain | W3C validator |