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 3017 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon1bd.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) | |
3 | 1, 2 | syl5bir 244 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓)) |
4 | 3 | con1d 147 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → 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: necon4ad 3035 fvclss 6992 suppssr 7852 suppofssd 7858 eceqoveq 8392 fofinf1o 8788 cantnfp1lem3 9132 cantnfp1 9133 mul0or 11269 inelr 11617 rimul 11618 rlimuni 14897 pc2dvds 16205 divsfval 16810 pleval2i 17564 lssvs0or 19813 lspsnat 19848 lmmo 21918 filssufilg 22449 hausflimi 22518 fclscf 22563 xrsmopn 23349 rectbntr0 23369 bcth3 23863 limcco 24420 ig1pdvds 24699 plyco0 24711 plypf1 24731 coeeulem 24743 coeidlem 24756 coeid3 24759 coemullem 24769 coemulhi 24773 coemulc 24774 dgradd2 24787 vieta1lem2 24829 dvtaylp 24887 musum 25696 perfectlem2 25734 dchrelbas3 25742 dchrmulid2 25756 dchreq 25762 dchrsum 25773 gausslemma2dlem4 25873 dchrisum0re 26017 coltr 26361 lmieu 26498 elspansn5 29279 atomli 30087 pthisspthorcycl 32273 onsucconni 33683 poimirlem8 34782 poimirlem9 34783 poimirlem18 34792 poimirlem21 34795 poimirlem22 34796 poimirlem26 34800 lshpcmp 36006 lsator0sp 36019 atnle 36335 atlatmstc 36337 osumcllem8N 36981 osumcllem11N 36984 pexmidlem5N 36992 pexmidlem8N 36995 dochsat0 38475 dochexmidlem5 38482 dochexmidlem8 38485 congabseq 39451 perfectALTVlem2 43734 |
Copyright terms: Public domain | W3C validator |