| 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 2941 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
| 2 | necon1bd.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) | |
| 3 | 1, 2 | biimtrrid 243 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓)) |
| 4 | 3 | con1d 145 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → 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: necon4ad 2959 fvclss 7261 suppssr 8220 suppssrg 8221 suppofssd 8228 eceqoveq 8862 fofinf1o 9372 cantnfp1lem3 9720 cantnfp1 9721 mul0or 11903 inelr 12256 rimul 12257 rlimuni 15586 pc2dvds 16917 divsfval 17592 pleval2i 18381 lssvs0or 21112 lspsnat 21147 psdmul 22170 lmmo 23388 filssufilg 23919 hausflimi 23988 fclscf 24033 xrsmopn 24834 rectbntr0 24854 bcth3 25365 limcco 25928 ig1pdvds 26219 plyco0 26231 plypf1 26251 coeeulem 26263 coeidlem 26276 coeid3 26279 coemullem 26289 coemulhi 26293 coemulc 26294 dgradd2 26308 vieta1lem2 26353 dvtaylp 26412 musum 27234 perfectlem2 27274 dchrelbas3 27282 dchrmullid 27296 dchreq 27302 dchrsum 27313 gausslemma2dlem4 27413 dchrisum0re 27557 muls0ord 28211 coltr 28655 lmieu 28792 pthisspthorcycl 29822 elspansn5 31593 atomli 32401 onsucconni 36438 poimirlem8 37635 poimirlem9 37636 poimirlem18 37645 poimirlem21 37648 poimirlem22 37649 poimirlem26 37653 lshpcmp 38989 lsator0sp 39002 atnle 39318 atlatmstc 39320 osumcllem8N 39965 osumcllem11N 39968 pexmidlem5N 39976 pexmidlem8N 39979 dochsat0 41459 dochexmidlem5 41466 dochexmidlem8 41469 aks6d1c4 42125 fsuppind 42600 congabseq 42986 dflim5 43342 mnringmulrcld 44247 perfectALTVlem2 47709 |
| Copyright terms: Public domain | W3C validator |