![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon3bd | Structured version Visualization version GIF version |
Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
necon3bd.1 | ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) |
Ref | Expression |
---|---|
necon3bd | ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nne 2966 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
2 | necon3bd.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
3 | 1, 2 | syl5bi 234 | . 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓)) |
4 | 3 | con1d 142 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1508 ≠ wne 2962 |
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 199 df-ne 2963 |
This theorem is referenced by: necon2ad 2977 nelne1OLD 3060 nelne2OLD 3062 nssne1 3912 nssne2 3913 disjne 4282 nbrne1 4945 nbrne2 4946 peano5 7419 oeeui 8028 domdifsn 8395 ac6sfi 8556 inf3lem2 8885 cnfcom3lem 8959 dfac9 9355 fin23lem21 9558 dedekindle 10603 zneo 11877 modirr 13124 sqrmo 14471 reusq0 14682 pc2dvds 16070 pcadd 16080 oddprmdvds 16094 4sqlem11 16146 latnlej 17549 sylow2blem3 18521 irredn0 19189 irredn1 19192 lssvneln0 19458 lspsnne2 19625 lspfixed 19635 lspindpi 19639 lsmcv 19648 lspsolv 19650 isnzr2 19770 coe1tmmul 20164 dfac14 21946 fbdmn0 22162 filufint 22248 flimfnfcls 22356 alexsubALTlem2 22376 evth 23282 cphsqrtcl2 23509 ovolicc2lem4 23840 lhop1lem 24329 lhop1 24330 lhop2 24331 lhop 24332 deg1add 24416 abelthlem2 24739 logcnlem2 24943 angpined 25125 asinneg 25181 dmgmaddn0 25318 lgsne0 25629 lgsqr 25645 lgsquadlem2 25675 lgsquadlem3 25676 axlowdimlem17 26463 spansncvi 29226 broutsideof2 33137 unblimceq0lem 33398 poimirlem28 34394 dvasin 34452 dvacos 34453 nninfnub 34501 dvrunz 34707 lsatcvatlem 35663 lkrlsp2 35717 opnlen0 35802 2llnne2N 36022 lnnat 36041 llnn0 36130 lplnn0N 36161 lplnllnneN 36170 llncvrlpln2 36171 llncvrlpln 36172 lvoln0N 36205 lplncvrlvol2 36229 lplncvrlvol 36230 dalempnes 36265 dalemqnet 36266 dalemcea 36274 dalem3 36278 cdlema1N 36405 cdlemb 36408 paddasslem5 36438 llnexchb2lem 36482 osumcllem4N 36573 pexmidlem1N 36584 lhp2lt 36615 lhp2atne 36648 lhp2at0ne 36650 4atexlemunv 36680 4atexlemex2 36685 trlne 36799 trlval4 36802 cdlemc4 36808 cdleme11dN 36876 cdleme11h 36880 cdlemednuN 36914 cdleme20j 36932 cdleme20k 36933 cdleme21at 36942 cdleme35f 37068 cdlemg11b 37256 dia2dimlem1 37678 dihmeetlem3N 37919 dihmeetlem15N 37935 dochsnnz 38064 dochexmidlem1 38074 dochexmidlem7 38080 mapdindp3 38336 fltne 38713 pellexlem1 38856 dfac21 39096 pm13.14 40192 uzlidlring 43594 suppdm 43963 |
Copyright terms: Public domain | W3C validator |