| 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 2965 | . 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵) |
| 3 | 2 | neqned 2947 | 1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ≠ wne 2940 |
| 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 207 df-ne 2941 |
| This theorem is referenced by: difn0 4367 imadisjlnd 6099 xpnz 6179 unixp 6302 inf3lem2 9669 infeq5 9677 cantnflem1 9729 iunfictbso 10154 rankcf 10817 hashfun 14476 hashge3el3dif 14526 abssubne0 15355 expnprm 16940 grpn0 18989 pmtr3ncomlem2 19492 pgpfaclem2 20102 isdrng2 20743 gzrngunit 21451 zringunit 21477 prmirredlem 21483 uvcf1 21812 lindfrn 21841 mpfrcl 22109 ply1frcl 22322 dfac14lem 23625 flimclslem 23992 lebnumlem3 24995 pmltpclem2 25484 i1fmullem 25729 fta1glem1 26207 fta1blem 26210 dgrcolem1 26313 plydivlem4 26338 plyrem 26347 facth 26348 fta1lem 26349 vieta1lem1 26352 vieta1lem2 26353 vieta1 26354 aalioulem2 26375 geolim3 26381 logcj 26648 argregt0 26652 argimgt0 26654 argimlt0 26655 logneg2 26657 tanarg 26661 logtayl 26702 cxpsqrt 26745 cxpcn3lem 26790 cxpcn3 26791 dcubic2 26887 dcubic 26889 cubic 26892 asinlem 26911 atandmcj 26952 atancj 26953 atanlogsublem 26958 bndatandm 26972 birthdaylem1 26994 basellem4 27127 dchrn0 27294 lgsne0 27379 usgr2trlncl 29780 nmlno0lem 30812 nmlnop0iALT 32014 eldmne0 32638 preimane 32680 prmidl0 33478 constrrtll 33772 cntnevol 34229 signsvtn0 34585 signstfveq0a 34591 signstfveq0 34592 nepss 35718 elima4 35776 heicant 37662 totbndbnd 37796 cdleme3c 40232 cdleme7e 40249 sn-1ne2 42300 sn-0ne2 42436 uvcn0 42552 compne 44460 stoweidlem39 46054 rrx2vlinest 48662 rrx2linesl 48664 elfvne0 48758 |
| Copyright terms: Public domain | W3C validator |