necon3i - Metamath Proof Explorer

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

Theorem necon3i 2674

Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)

**Hypothesis**
Ref	Expression
necon3i.1

**Assertion**
Ref	Expression
necon3i

**Proof of Theorem necon3i**
Step	Hyp	Ref	Expression
1		necon3i.1	. 2
2		id 22	. . 3
3	2	necon3d 2670	. 2
4	1, 3	ax-mp 5	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1369

wne 2620

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 185 df-ne 2622

This theorem is referenced by: xpnz 5278 unixp 5391 inf3lem2 7856 infeq5 7864 cantnflem1 7918 cantnflem1OLD 7941 iunfictbso 8305 rankcf 8965 hashge3el3dif 12208 hashfun 12220 s1nz 12318 abssubne0 12825 expnprm 13985 grpn0 15591 pmtr3ncomlem2 16001 gsumval3OLD 16403 pgpfaclem2 16605 isdrng2 16864 mpfrcl 17626 ply1frcl 17775 gzrngunit 17900 zringunit 17936 zrngunit 17937 prmirredlem 17939 prmirredlemOLD 17942 uvcf1 18239 lindfrn 18272 dfac14lem 19212 flimclslem 19579 lebnumlem3 20557 pmltpclem2 20955 i1fmullem 21194 fta1glem1 21659 fta1blem 21662 dgrcolem1 21762 plydivlem4 21784 plyrem 21793 facth 21794 fta1lem 21795 vieta1lem1 21798 vieta1lem2 21799 vieta1 21800 aalioulem2 21821 geolim3 21827 logcj 22077 argregt0 22081 argimgt0 22083 argimlt0 22084 logneg2 22086 tanarg 22090 logtayl 22127 cxpsqr 22170 cxpcn3lem 22207 cxpcn3 22208 dcubic2 22261 dcubic 22263 cubic 22266 asinlem 22285 atandmcj 22326 atancj 22327 atanlogsublem 22332 bndatandm 22346 birthdaylem1 22367 basellem4 22443 basellem5 22444 dchrn0 22611 lgsne0 22694 constr3lem2 23554 nmlno0lem 24215 nmlnop0iALT 25421 difneqnul 25920 cntnevol 26664 signsvtn0 26993 signstfveq0a 26999 signstfveq0 27000 nepss 27396 elima4 27612 heicant 28452 totbndbnd 28714 compne 29722 stoweidlem39 29860 cdleme3c 33970 cdleme7e 33987