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 2795 | . . 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 1483 ≠ wne 2794 |
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 2795 |
This theorem is referenced by: necon4ad 2813 fvclss 6500 suppssr 7326 eceqoveq 7853 fofinf1o 8241 cantnfp1lem3 8577 cantnfp1 8578 mul0or 10667 inelr 11010 rimul 11011 rlimuni 14281 pc2dvds 15583 divsfval 16207 pleval2i 16964 lssvs0or 19110 lspsnat 19145 lmmo 21184 filssufilg 21715 hausflimi 21784 fclscf 21829 xrsmopn 22615 rectbntr0 22635 bcth3 23128 limcco 23657 ig1pdvds 23936 plyco0 23948 plypf1 23968 coeeulem 23980 coeidlem 23993 coeid3 23996 coemullem 24006 coemulhi 24010 coemulc 24011 dgradd2 24024 vieta1lem2 24066 dvtaylp 24124 musum 24917 perfectlem2 24955 dchrelbas3 24963 dchrmulid2 24977 dchreq 24983 dchrsum 24994 gausslemma2dlem4 25094 dchrisum0re 25202 coltr 25542 lmieu 25676 elspansn5 28433 atomli 29241 onsucconni 32436 poimirlem8 33417 poimirlem9 33418 poimirlem18 33427 poimirlem21 33430 poimirlem22 33431 poimirlem26 33435 lshpcmp 34275 lsator0sp 34288 atnle 34604 atlatmstc 34606 osumcllem8N 35249 osumcllem11N 35252 pexmidlem5N 35260 pexmidlem8N 35263 dochsat0 36746 dochexmidlem5 36753 dochexmidlem8 36756 congabseq 37541 perfectALTVlem2 41631 |
Copyright terms: Public domain | W3C validator |