![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon1bd | Structured version Visualization version GIF version |
Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
Ref | Expression |
---|---|
necon1bd.1 | ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) |
Ref | Expression |
---|---|
necon1bd | ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2939 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon1bd.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) | |
3 | 1, 2 | biimtrrid 242 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓)) |
4 | 3 | con1d 145 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ≠ wne 2938 |
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 2939 |
This theorem is referenced by: necon4ad 2957 fvclss 7242 suppssr 8183 suppssrg 8184 suppofssd 8190 eceqoveq 8818 fofinf1o 9329 cantnfp1lem3 9677 cantnfp1 9678 mul0or 11858 inelr 12206 rimul 12207 rlimuni 15498 pc2dvds 16816 divsfval 17497 pleval2i 18293 lssvs0or 20868 lspsnat 20903 lmmo 23104 filssufilg 23635 hausflimi 23704 fclscf 23749 xrsmopn 24548 rectbntr0 24568 bcth3 25079 limcco 25642 ig1pdvds 25929 plyco0 25941 plypf1 25961 coeeulem 25973 coeidlem 25986 coeid3 25989 coemullem 25999 coemulhi 26003 coemulc 26004 dgradd2 26018 vieta1lem2 26060 dvtaylp 26118 musum 26931 perfectlem2 26969 dchrelbas3 26977 dchrmullid 26991 dchreq 26997 dchrsum 27008 gausslemma2dlem4 27108 dchrisum0re 27252 coltr 28165 lmieu 28302 elspansn5 31094 atomli 31902 pthisspthorcycl 34417 onsucconni 35625 poimirlem8 36799 poimirlem9 36800 poimirlem18 36809 poimirlem21 36812 poimirlem22 36813 poimirlem26 36817 lshpcmp 38161 lsator0sp 38174 atnle 38490 atlatmstc 38492 osumcllem8N 39137 osumcllem11N 39140 pexmidlem5N 39148 pexmidlem8N 39151 dochsat0 40631 dochexmidlem5 40638 dochexmidlem8 40641 fsuppind 41464 congabseq 42015 dflim5 42381 mnringmulrcld 43289 perfectALTVlem2 46688 |
Copyright terms: Public domain | W3C validator |