![]() |
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 242 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓)) |
4 | 3 | con1d 145 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ 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 206 df-ne 2941 |
This theorem is referenced by: necon4ad 2959 fvclss 7193 suppssr 8131 suppssrg 8132 suppofssd 8138 eceqoveq 8767 fofinf1o 9277 cantnfp1lem3 9624 cantnfp1 9625 mul0or 11803 inelr 12151 rimul 12152 rlimuni 15441 pc2dvds 16759 divsfval 17437 pleval2i 18233 lssvs0or 20616 lspsnat 20651 lmmo 22754 filssufilg 23285 hausflimi 23354 fclscf 23399 xrsmopn 24198 rectbntr0 24218 bcth3 24718 limcco 25280 ig1pdvds 25564 plyco0 25576 plypf1 25596 coeeulem 25608 coeidlem 25621 coeid3 25624 coemullem 25634 coemulhi 25638 coemulc 25639 dgradd2 25652 vieta1lem2 25694 dvtaylp 25752 musum 26563 perfectlem2 26601 dchrelbas3 26609 dchrmulid2 26623 dchreq 26629 dchrsum 26640 gausslemma2dlem4 26740 dchrisum0re 26884 coltr 27638 lmieu 27775 elspansn5 30565 atomli 31373 pthisspthorcycl 33786 onsucconni 34962 poimirlem8 36136 poimirlem9 36137 poimirlem18 36146 poimirlem21 36149 poimirlem22 36150 poimirlem26 36154 lshpcmp 37500 lsator0sp 37513 atnle 37829 atlatmstc 37831 osumcllem8N 38476 osumcllem11N 38479 pexmidlem5N 38487 pexmidlem8N 38490 dochsat0 39970 dochexmidlem5 39977 dochexmidlem8 39980 fsuppind 40812 congabseq 41345 dflim5 41711 mnringmulrcld 42600 perfectALTVlem2 46004 |
Copyright terms: Public domain | W3C validator |