![]() |
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 2824 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon1bd.1 | . . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓)) | |
3 | 1, 2 | syl5bir 233 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓)) |
4 | 3 | con1d 139 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1523 ≠ wne 2823 |
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 197 df-ne 2824 |
This theorem is referenced by: necon4ad 2842 fvclss 6540 suppssr 7371 eceqoveq 7895 fofinf1o 8282 cantnfp1lem3 8615 cantnfp1 8616 mul0or 10705 inelr 11048 rimul 11049 rlimuni 14325 pc2dvds 15630 divsfval 16254 pleval2i 17011 lssvs0or 19158 lspsnat 19193 lmmo 21232 filssufilg 21762 hausflimi 21831 fclscf 21876 xrsmopn 22662 rectbntr0 22682 bcth3 23174 limcco 23702 ig1pdvds 23981 plyco0 23993 plypf1 24013 coeeulem 24025 coeidlem 24038 coeid3 24041 coemullem 24051 coemulhi 24055 coemulc 24056 dgradd2 24069 vieta1lem2 24111 dvtaylp 24169 musum 24962 perfectlem2 25000 dchrelbas3 25008 dchrmulid2 25022 dchreq 25028 dchrsum 25039 gausslemma2dlem4 25139 dchrisum0re 25247 coltr 25587 lmieu 25721 elspansn5 28561 atomli 29369 onsucconni 32561 poimirlem8 33547 poimirlem9 33548 poimirlem18 33557 poimirlem21 33560 poimirlem22 33561 poimirlem26 33565 lshpcmp 34593 lsator0sp 34606 atnle 34922 atlatmstc 34924 osumcllem8N 35567 osumcllem11N 35570 pexmidlem5N 35578 pexmidlem8N 35581 dochsat0 37063 dochexmidlem5 37070 dochexmidlem8 37073 congabseq 37858 perfectALTVlem2 41956 |
Copyright terms: Public domain | W3C validator |