![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3ad | Structured version Visualization version Unicode version |
Description: Contrapositive law deduction 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 |
---|---|
necon3ad.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
necon3ad |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3ad.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | id 22 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | neneqd 2631 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | nsyli 147 |
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 189 df-ne 2626 |
This theorem is referenced by: necon1ad 2643 necon3d 2647 disjpss 3817 oeeulem 7307 enp1i 7811 canthp1lem2 9083 winalim2 9126 nlt1pi 9336 sqreulem 13434 rpnnen2lem11 14289 dvdseq 14364 eucalglt 14556 nprm 14650 pcprmpw2 14843 pcmpt 14849 expnprm 14859 prmlem0 15089 pltnle 16224 psgnunilem1 17146 pgpfi 17269 frgpnabllem1 17521 gsumval3a 17549 ablfac1eulem 17717 pgpfaclem2 17727 lspdisjb 18361 lspdisj2 18362 obselocv 19303 0nnei 20140 t0dist 20353 t1sep 20398 ordthauslem 20411 hausflim 21008 bcthlem5 22308 bcth 22309 fta1g 23130 plyco0 23158 dgrnznn 23213 coeaddlem 23215 fta1 23273 vieta1lem2 23276 logcnlem3 23601 dvloglem 23605 dcubic 23784 mumullem2 24119 2sqlem8a 24311 dchrisum0flblem1 24358 colperpexlem2 24785 ocnel 26963 hatomistici 28027 sibfof 29185 outsideofrflx 30906 poimirlem23 31975 mblfinlem1 31989 cntotbnd 32140 heiborlem6 32160 lshpnel 32561 lshpcmp 32566 lfl1 32648 lkrshp 32683 lkrpssN 32741 atnlt 32891 atnle 32895 atlatmstc 32897 intnatN 32984 atbtwn 33023 llnnlt 33100 lplnnlt 33142 2llnjaN 33143 lvolnltN 33195 2lplnja 33196 dalem-cly 33248 dalem44 33293 2llnma3r 33365 cdlemblem 33370 lhpm0atN 33606 lhp2atnle 33610 cdlemednpq 33877 cdleme22cN 33921 cdlemg18b 34258 cdlemg42 34308 dia2dimlem1 34644 dochkrshp 34966 hgmapval0 35475 2f1fvneq 39024 uspgrloopnb0 39566 |
Copyright terms: Public domain | W3C validator |