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 3041 | . 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 3023 | 1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ≠ wne 3016 |
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 3017 |
This theorem is referenced by: difn0 4323 xpnz 6010 unixp 6127 inf3lem2 9081 infeq5 9089 cantnflem1 9141 iunfictbso 9529 rankcf 10188 hashfun 13788 hashge3el3dif 13834 abssubne0 14666 expnprm 16228 grpn0 18075 pmtr3ncomlem2 18533 pgpfaclem2 19135 isdrng2 19443 mpfrcl 20228 ply1frcl 20411 gzrngunit 20541 zringunit 20565 prmirredlem 20570 uvcf1 20866 lindfrn 20895 dfac14lem 22155 flimclslem 22522 lebnumlem3 23496 pmltpclem2 23979 i1fmullem 24224 fta1glem1 24688 fta1blem 24691 dgrcolem1 24792 plydivlem4 24814 plyrem 24823 facth 24824 fta1lem 24825 vieta1lem1 24828 vieta1lem2 24829 vieta1 24830 aalioulem2 24851 geolim3 24857 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 25457 basellem4 25589 dchrn0 25754 lgsne0 25839 usgr2trlncl 27469 nmlno0lem 28498 nmlnop0iALT 29700 eldmne0 30302 preimane 30344 cntnevol 31387 signsvtn0 31740 signstfveq0a 31746 signstfveq0 31747 nepss 32846 elima4 32917 heicant 34809 totbndbnd 34950 cdleme3c 37248 cdleme7e 37265 sn-1ne2 39038 sn-0ne2 39116 imadisjlnd 40391 compne 40653 stoweidlem39 42205 rrx2vlinest 44626 rrx2linesl 44628 |
Copyright terms: Public domain | W3C validator |