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 2807 | . 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 2789 | 1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ≠ wne 2780 |
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 196 df-ne 2782 |
This theorem is referenced by: difn0 3897 xpnz 5472 unixp 5585 inf3lem2 8409 infeq5 8417 cantnflem1 8469 iunfictbso 8820 rankcf 9478 hashfun 13084 hashge3el3dif 13122 s1nzOLD 13240 abssubne0 13904 expnprm 15444 grpn0 17277 pmtr3ncomlem2 17717 pgpfaclem2 18304 isdrng2 18580 mpfrcl 19339 ply1frcl 19504 gzrngunit 19631 zringunit 19655 prmirredlem 19660 uvcf1 19950 lindfrn 19979 dfac14lem 21230 flimclslem 21598 lebnumlem3 22570 pmltpclem2 23025 i1fmullem 23267 fta1glem1 23729 fta1blem 23732 dgrcolem1 23833 plydivlem4 23855 plyrem 23864 facth 23865 fta1lem 23866 vieta1lem1 23869 vieta1lem2 23870 vieta1 23871 aalioulem2 23892 geolim3 23898 logcj 24156 argregt0 24160 argimgt0 24162 argimlt0 24163 logneg2 24165 tanarg 24169 logtayl 24206 cxpsqrt 24249 cxpcn3lem 24288 cxpcn3 24289 dcubic2 24371 dcubic 24373 cubic 24376 asinlem 24395 atandmcj 24436 atancj 24437 atanlogsublem 24442 bndatandm 24456 birthdaylem1 24478 basellem4 24610 basellem5 24611 dchrn0 24775 lgsne0 24860 constr3lem2 26174 nmlno0lem 27032 nmlnop0iALT 28238 cntnevol 29618 signsvtn0 29973 signstfveq0a 29979 signstfveq0 29980 nepss 30854 elima4 30924 heicant 32614 totbndbnd 32758 cdleme3c 34535 cdleme7e 34552 imadisjlnd 37479 compne 37665 stoweidlem39 38932 usgr2trlncl 40966 |
Copyright terms: Public domain | W3C validator |