![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3i | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
Ref | Expression |
---|---|
necon3i.1 | ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
necon3i | ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3i.1 | . . 3 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) | |
2 | 1 | necon3ai 2968 | . 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 2950 | 1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 ≠ wne 2943 |
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 2944 |
This theorem is referenced by: difn0 4091 xpnz 5693 unixp 5811 inf3lem2 8694 infeq5 8702 cantnflem1 8754 iunfictbso 9141 rankcf 9805 hashfun 13426 hashge3el3dif 13470 abssubne0 14264 expnprm 15813 grpn0 17662 pmtr3ncomlem2 18101 pgpfaclem2 18689 isdrng2 18967 mpfrcl 19733 ply1frcl 19898 gzrngunit 20027 zringunit 20051 prmirredlem 20056 uvcf1 20348 lindfrn 20377 dfac14lem 21641 flimclslem 22008 lebnumlem3 22982 pmltpclem2 23437 i1fmullem 23681 fta1glem1 24145 fta1blem 24148 dgrcolem1 24249 plydivlem4 24271 plyrem 24280 facth 24281 fta1lem 24282 vieta1lem1 24285 vieta1lem2 24286 vieta1 24287 aalioulem2 24308 geolim3 24314 logcj 24573 argregt0 24577 argimgt0 24579 argimlt0 24580 logneg2 24582 tanarg 24586 logtayl 24627 cxpsqrt 24670 cxpcn3lem 24709 cxpcn3 24710 dcubic2 24792 dcubic 24794 cubic 24797 asinlem 24816 atandmcj 24857 atancj 24858 atanlogsublem 24863 bndatandm 24877 birthdaylem1 24899 basellem4 25031 basellem5 25032 dchrn0 25196 lgsne0 25281 usgr2trlncl 26891 nmlno0lem 27988 nmlnop0iALT 29194 cntnevol 30631 signsvtn0 30987 signstfveq0a 30993 signstfveq0 30994 nepss 31937 elima4 32015 heicant 33776 totbndbnd 33918 cdleme3c 36038 cdleme7e 36055 imadisjlnd 38983 compne 39167 compneOLD 39168 stoweidlem39 40768 |
Copyright terms: Public domain | W3C validator |