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 2786 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
2 | necon3bd.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
3 | 1, 2 | syl5bi 231 | . 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓)) |
4 | 3 | con1d 138 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1475 ≠ wne 2780 |
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 196 df-ne 2782 |
This theorem is referenced by: necon2ad 2797 nelne1 2878 nelne2 2879 nssne1 3624 nssne2 3625 disjne 3974 nbrne1 4602 nbrne2 4603 peano5 6981 oeeui 7569 domdifsn 7928 ac6sfi 8089 inf3lem2 8409 cnfcom3lem 8483 dfac9 8841 fin23lem21 9044 dedekindle 10080 zneo 11336 modirr 12603 sqrmo 13840 pc2dvds 15421 pcadd 15431 oddprmdvds 15445 4sqlem11 15497 latnlej 16891 sylow2blem3 17860 irredn0 18526 irredn1 18529 lssneln0 18773 lspsnne2 18939 lspfixed 18949 lspindpi 18953 lsmcv 18962 lspsolv 18964 isnzr2 19084 coe1tmmul 19468 dfac14 21231 fbdmn0 21448 filufint 21534 flimfnfcls 21642 alexsubALTlem2 21662 evth 22566 cphsqrtcl2 22794 ovolicc2lem4 23095 lhop1lem 23580 lhop1 23581 lhop2 23582 lhop 23583 deg1add 23667 abelthlem2 23990 logcnlem2 24189 angpined 24357 asinneg 24413 dmgmaddn0 24549 lgsne0 24860 lgsqr 24876 lgsquadlem2 24906 lgsquadlem3 24907 axlowdimlem17 25638 spansncvi 27895 broutsideof2 31399 unblimceq0lem 31667 poimirlem28 32607 dvasin 32666 dvacos 32667 nninfnub 32717 dvrunz 32923 lsatcvatlem 33354 lkrlsp2 33408 opnlen0 33493 2llnne2N 33712 lnnat 33731 llnn0 33820 lplnn0N 33851 lplnllnneN 33860 llncvrlpln2 33861 llncvrlpln 33862 lvoln0N 33895 lplncvrlvol2 33919 lplncvrlvol 33920 dalempnes 33955 dalemqnet 33956 dalemcea 33964 dalem3 33968 cdlema1N 34095 cdlemb 34098 paddasslem5 34128 llnexchb2lem 34172 osumcllem4N 34263 pexmidlem1N 34274 lhp2lt 34305 lhp2atne 34338 lhp2at0ne 34340 4atexlemunv 34370 4atexlemex2 34375 trlne 34490 trlval4 34493 cdlemc4 34499 cdleme11dN 34567 cdleme11h 34571 cdlemednuN 34605 cdleme20j 34624 cdleme20k 34625 cdleme21at 34634 cdleme35f 34760 cdlemg11b 34948 dia2dimlem1 35371 dihmeetlem3N 35612 dihmeetlem15N 35628 dochsnnz 35757 dochexmidlem1 35767 dochexmidlem7 35773 mapdindp3 36029 pellexlem1 36411 dfac21 36654 pm13.14 37632 uzlidlring 41719 suppdm 42094 |
Copyright terms: Public domain | W3C validator |