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 3038 | . 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 3020 | 1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3013 |
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 208 df-ne 3014 |
This theorem is referenced by: difn0 4321 xpnz 6009 unixp 6126 inf3lem2 9080 infeq5 9088 cantnflem1 9140 iunfictbso 9528 rankcf 10187 hashfun 13786 hashge3el3dif 13832 abssubne0 14664 expnprm 16226 grpn0 18073 pmtr3ncomlem2 18531 pgpfaclem2 19133 isdrng2 19441 mpfrcl 20226 ply1frcl 20409 gzrngunit 20539 zringunit 20563 prmirredlem 20568 uvcf1 20864 lindfrn 20893 dfac14lem 22153 flimclslem 22520 lebnumlem3 23494 pmltpclem2 23977 i1fmullem 24222 fta1glem1 24686 fta1blem 24689 dgrcolem1 24790 plydivlem4 24812 plyrem 24821 facth 24822 fta1lem 24823 vieta1lem1 24826 vieta1lem2 24827 vieta1 24828 aalioulem2 24849 geolim3 24855 logcj 25116 argregt0 25120 argimgt0 25122 argimlt0 25123 logneg2 25125 tanarg 25129 logtayl 25170 cxpsqrt 25213 cxpcn3lem 25255 cxpcn3 25256 dcubic2 25349 dcubic 25351 cubic 25354 asinlem 25373 atandmcj 25414 atancj 25415 atanlogsublem 25420 bndatandm 25434 birthdaylem1 25456 basellem4 25588 dchrn0 25753 lgsne0 25838 usgr2trlncl 27468 nmlno0lem 28497 nmlnop0iALT 29699 eldmne0 30301 preimane 30343 cntnevol 31386 signsvtn0 31739 signstfveq0a 31745 signstfveq0 31746 nepss 32845 elima4 32916 heicant 34808 totbndbnd 34948 cdleme3c 37246 cdleme7e 37263 sn-1ne2 39036 sn-0ne2 39114 imadisjlnd 40389 compne 40650 stoweidlem39 42201 rrx2vlinest 44656 rrx2linesl 44658 |
Copyright terms: Public domain | W3C validator |