necon3i - Metamath Proof Explorer

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

Theorem necon3i 2640

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 2636	. 2
4	1, 3	ax-mp 5	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1362

wne 2596

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 2598

This theorem is referenced by: xpnz 5245 unixp 5358 inf3lem2 7823 infeq5 7831 cantnflem1 7885 cantnflem1OLD 7908 iunfictbso 8272 rankcf 8931 hashge3el3dif 12170 hashfun 12182 s1nz 12280 abssubne0 12787 expnprm 13946 grpn0 15549 pmtr3ncomlem2 15959 gsumval3OLD 16361 pgpfaclem2 16556 isdrng2 16765 gzrngunit 17721 zringunit 17755 zrngunit 17756 prmirredlem 17758 prmirredlemOLD 17761 uvcf1 18058 lindfrn 18091 dfac14lem 19031 flimclslem 19398 lebnumlem3 20376 pmltpclem2 20774 i1fmullem 21013 mpfrcl 21369 fta1glem1 21521 fta1blem 21524 dgrcolem1 21624 plydivlem4 21646 plyrem 21655 facth 21656 fta1lem 21657 vieta1lem1 21660 vieta1lem2 21661 vieta1 21662 aalioulem2 21683 geolim3 21689 logcj 21939 argregt0 21943 argimgt0 21945 argimlt0 21946 logneg2 21948 tanarg 21952 logtayl 21989 cxpsqr 22032 cxpcn3lem 22069 cxpcn3 22070 dcubic2 22123 dcubic 22125 cubic 22128 asinlem 22147 atandmcj 22188 atancj 22189 atanlogsublem 22194 bndatandm 22208 birthdaylem1 22229 basellem4 22305 basellem5 22306 dchrn0 22473 lgsne0 22556 constr3lem2 23354 nmlno0lem 24015 nmlnop0iALT 25221 difneqnul 25721 cntnevol 26495 signsvtn0 26818 signstfveq0a 26824 signstfveq0 26825 nepss 27220 elima4 27436 heicant 28267 totbndbnd 28529 compne 29538 stoweidlem39 29677 cdleme3c 33444 cdleme7e 33461