Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon1ai | Structured version Visualization version Unicode version |
Description: Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
Ref | Expression |
---|---|
necon1ai.1 |
Ref | Expression |
---|---|
necon1ai |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon1ai.1 | . . 3 | |
2 | 1 | necon3ai 2819 | . 2 |
3 | 2 | notnotrd 128 | 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: necon1i 2827 opnz 4942 inisegn0 5497 tz6.12i 6214 elfvdm 6220 fvfundmfvn0 6226 brfvopabrbr 6279 elfvmptrab1 6305 brovpreldm 7254 brovex 7348 brwitnlem 7587 cantnflem1 8586 carddomi2 8796 cdainf 9014 rankcf 9599 1re 10039 eliooxr 12232 iccssioo2 12246 elfzoel1 12468 elfzoel2 12469 ismnd 17297 lactghmga 17824 pmtrmvd 17876 mpfrcl 19518 fsubbas 21671 filuni 21689 ptcmplem2 21857 itg1climres 23481 mbfi1fseqlem4 23485 dvferm1lem 23747 dvferm2lem 23749 dvferm 23751 dvivthlem1 23771 coeeq2 23998 coe1termlem 24014 isppw 24840 dchrelbasd 24964 lgsne0 25060 wlkvv 26522 eldm3 31651 brfvimex 38324 brovmptimex 38325 clsneibex 38400 neicvgbex 38410 afvnufveq 41227 |
Copyright terms: Public domain | W3C validator |