![]() |
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 2940 | . . 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 1541 ≠ wne 2939 |
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 2940 |
This theorem is referenced by: necon4ad 2958 fvclss 7225 suppssr 8163 suppssrg 8164 suppofssd 8170 eceqoveq 8799 fofinf1o 9310 cantnfp1lem3 9657 cantnfp1 9658 mul0or 11836 inelr 12184 rimul 12185 rlimuni 15476 pc2dvds 16794 divsfval 17475 pleval2i 18271 lssvs0or 20672 lspsnat 20707 lmmo 22813 filssufilg 23344 hausflimi 23413 fclscf 23458 xrsmopn 24257 rectbntr0 24277 bcth3 24777 limcco 25339 ig1pdvds 25623 plyco0 25635 plypf1 25655 coeeulem 25667 coeidlem 25680 coeid3 25683 coemullem 25693 coemulhi 25697 coemulc 25698 dgradd2 25711 vieta1lem2 25753 dvtaylp 25811 musum 26622 perfectlem2 26660 dchrelbas3 26668 dchrmullid 26682 dchreq 26688 dchrsum 26699 gausslemma2dlem4 26799 dchrisum0re 26943 coltr 27763 lmieu 27900 elspansn5 30690 atomli 31498 pthisspthorcycl 33950 onsucconni 35126 poimirlem8 36300 poimirlem9 36301 poimirlem18 36310 poimirlem21 36313 poimirlem22 36314 poimirlem26 36318 lshpcmp 37663 lsator0sp 37676 atnle 37992 atlatmstc 37994 osumcllem8N 38639 osumcllem11N 38642 pexmidlem5N 38650 pexmidlem8N 38653 dochsat0 40133 dochexmidlem5 40140 dochexmidlem8 40143 fsuppind 40951 congabseq 41484 dflim5 41850 mnringmulrcld 42758 perfectALTVlem2 46162 |
Copyright terms: Public domain | W3C validator |