![]() |
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 2986 | . 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 2968 | 1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ≠ wne 2961 |
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 199 df-ne 2962 |
This theorem is referenced by: difn0 4204 xpnz 5850 unixp 5965 inf3lem2 8880 infeq5 8888 cantnflem1 8940 iunfictbso 9328 rankcf 9991 hashfun 13605 hashge3el3dif 13649 abssubne0 14531 expnprm 16088 grpn0 17917 pmtr3ncomlem2 18357 pgpfaclem2 18948 isdrng2 19229 mpfrcl 20005 ply1frcl 20178 gzrngunit 20307 zringunit 20331 prmirredlem 20336 uvcf1 20632 lindfrn 20661 dfac14lem 21923 flimclslem 22290 lebnumlem3 23264 pmltpclem2 23747 i1fmullem 23992 fta1glem1 24456 fta1blem 24459 dgrcolem1 24560 plydivlem4 24582 plyrem 24591 facth 24592 fta1lem 24593 vieta1lem1 24596 vieta1lem2 24597 vieta1 24598 aalioulem2 24619 geolim3 24625 logcj 24884 argregt0 24888 argimgt0 24890 argimlt0 24891 logneg2 24893 tanarg 24897 logtayl 24938 cxpsqrt 24981 cxpcn3lem 25023 cxpcn3 25024 dcubic2 25117 dcubic 25119 cubic 25122 asinlem 25141 atandmcj 25182 atancj 25183 atanlogsublem 25188 bndatandm 25202 birthdaylem1 25225 basellem4 25357 dchrn0 25522 lgsne0 25607 usgr2trlncl 27243 nmlno0lem 28341 nmlnop0iALT 29547 preimane 30171 cntnevol 31132 signsvtn0 31486 signsvtn0OLD 31487 signstfveq0a 31493 signstfveq0 31494 signstfveq0OLD 31495 nepss 32468 elima4 32539 heicant 34368 totbndbnd 34509 cdleme3c 36811 cdleme7e 36828 imadisjlnd 39874 compne 40191 compneOLD 40192 stoweidlem39 41755 rrx2vlinest 44096 rrx2linesl 44098 |
Copyright terms: Public domain | W3C validator |