![]() |
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 2966 | . 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 2948 | 1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ≠ wne 2941 |
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 206 df-ne 2942 |
This theorem is referenced by: difn0 4322 xpnz 6109 unixp 6232 inf3lem2 9561 infeq5 9569 cantnflem1 9621 iunfictbso 10046 rankcf 10709 hashfun 14329 hashge3el3dif 14377 abssubne0 15193 expnprm 16766 grpn0 18774 pmtr3ncomlem2 19247 pgpfaclem2 19852 isdrng2 20183 gzrngunit 20848 zringunit 20872 prmirredlem 20878 uvcf1 21183 lindfrn 21212 mpfrcl 21479 ply1frcl 21668 dfac14lem 22952 flimclslem 23319 lebnumlem3 24310 pmltpclem2 24797 i1fmullem 25042 fta1glem1 25514 fta1blem 25517 dgrcolem1 25618 plydivlem4 25640 plyrem 25649 facth 25650 fta1lem 25651 vieta1lem1 25654 vieta1lem2 25655 vieta1 25656 aalioulem2 25677 geolim3 25683 logcj 25945 argregt0 25949 argimgt0 25951 argimlt0 25952 logneg2 25954 tanarg 25958 logtayl 25999 cxpsqrt 26042 cxpcn3lem 26084 cxpcn3 26085 dcubic2 26178 dcubic 26180 cubic 26183 asinlem 26202 atandmcj 26243 atancj 26244 atanlogsublem 26249 bndatandm 26263 birthdaylem1 26285 basellem4 26417 dchrn0 26582 lgsne0 26667 usgr2trlncl 28594 nmlno0lem 29621 nmlnop0iALT 30823 eldmne0 31428 preimane 31472 prmidl0 32102 cntnevol 32696 signsvtn0 33051 signstfveq0a 33057 signstfveq0 33058 nepss 34158 elima4 34220 heicant 36080 totbndbnd 36215 cdleme3c 38660 cdleme7e 38677 uvcn0 40691 sn-1ne2 40719 sn-0ne2 40813 imadisjlnd 42375 compne 42663 stoweidlem39 44212 rrx2vlinest 46759 rrx2linesl 46761 elfvne0 46847 |
Copyright terms: Public domain | W3C validator |