necon3i - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > necon3i		Structured version Visualization version Unicode version

Theorem necon3i 2667

Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

**Hypothesis**
Ref	Expression
necon3i.1

**Assertion**
Ref	Expression
necon3i

**Proof of Theorem necon3i**
Step	Hyp	Ref	Expression
1		necon3i.1	. . 3
2	1	necon3ai 2660	. 2
3	2	neqned 2641	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1454

wne 2632

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 190 df-ne 2634

This theorem is referenced by: difn0 3835 xpnz 5274 unixp 5387 inf3lem2 8159 infeq5 8167 cantnflem1 8219 iunfictbso 8570 rankcf 9227 hashfun 12641 hashge3el3dif 12674 s1nz 12780 abssubne0 13427 expnprm 14895 grpn0 16746 pmtr3ncomlem2 17163 pgpfaclem2 17763 isdrng2 18033 mpfrcl 18789 ply1frcl 18955 gzrngunit 19081 zringunit 19110 prmirredlem 19112 uvcf1 19398 lindfrn 19427 dfac14lem 20680 flimclslem 21047 lebnumlem3 22039 lebnumlem3OLD 22042 pmltpclem2 22448 i1fmullem 22700 fta1glem1 23164 fta1blem 23167 dgrcolem1 23275 plydivlem4 23297 plyrem 23306 facth 23307 fta1lem 23308 vieta1lem1 23311 vieta1lem2 23312 vieta1 23313 aalioulem2 23337 geolim3 23343 logcj 23603 argregt0 23607 argimgt0 23609 argimlt0 23610 logneg2 23612 tanarg 23616 logtayl 23653 cxpsqrt 23696 cxpcn3lem 23735 cxpcn3 23736 dcubic2 23818 dcubic 23820 cubic 23823 asinlem 23842 atandmcj 23883 atancj 23884 atanlogsublem 23889 bndatandm 23903 birthdaylem1 23925 basellem4 24058 basellem5 24059 dchrn0 24226 lgsne0 24309 constr3lem2 25422 nmlno0lem 26482 nmlnop0iALT 27696 cntnevol 29098 signsvtn0 29507 signstfveq0a 29513 signstfveq0 29514 nepss 30398 elima4 30469 heicant 32019 totbndbnd 32165 cdleme3c 33840 cdleme7e 33857 imadisjlnd 36643 compne 36836 stoweidlem39 37937