| 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 2944 | . . 3 ⊢ (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) | |
| 2 | necon3bd.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) | |
| 3 | 1, 2 | biimtrid 242 | . 2 ⊢ (𝜑 → (¬ 𝐴 ≠ 𝐵 → 𝜓)) |
| 4 | 3 | con1d 145 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ 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 207 df-ne 2941 |
| This theorem is referenced by: necon2ad 2955 nssne1 4046 nssne2 4047 disjne 4455 nbrne1 5162 nbrne2 5163 peano5 7915 oeeui 8640 domdifsn 9094 ac6sfi 9320 inf3lem2 9669 cnfcom3lem 9743 dfac9 10177 fin23lem21 10379 dedekindle 11425 zneo 12701 modirr 13983 sqrmo 15290 reusq0 15501 pc2dvds 16917 pcadd 16927 oddprmdvds 16941 4sqlem11 16993 latnlej 18501 sylow2blem3 19640 irredn0 20423 irredn1 20426 isnzr2 20518 lssvneln0 20950 lspsnne2 21120 lspfixed 21130 lspindpi 21134 lsmcv 21143 lspsolv 21145 coe1tmmul 22280 dfac14 23626 fbdmn0 23842 filufint 23928 flimfnfcls 24036 alexsubALTlem2 24056 evth 24991 cphsqrtcl2 25220 ovolicc2lem4 25555 lhop1lem 26052 lhop1 26053 lhop2 26054 lhop 26055 deg1add 26142 abelthlem2 26476 logcnlem2 26685 angpined 26873 asinneg 26929 dmgmaddn0 27066 lgsne0 27379 lgsqr 27395 lgsquadlem2 27425 lgsquadlem3 27426 axlowdimlem17 28973 spansncvi 31671 zarcmplem 33880 broutsideof2 36123 unblimceq0lem 36507 poimirlem28 37655 dvasin 37711 dvacos 37712 nninfnub 37758 dvrunz 37961 lsatcvatlem 39050 lkrlsp2 39104 opnlen0 39189 2llnne2N 39410 lnnat 39429 llnn0 39518 lplnn0N 39549 lplnllnneN 39558 llncvrlpln2 39559 llncvrlpln 39560 lvoln0N 39593 lplncvrlvol2 39617 lplncvrlvol 39618 dalempnes 39653 dalemqnet 39654 dalemcea 39662 dalem3 39666 cdlema1N 39793 cdlemb 39796 paddasslem5 39826 llnexchb2lem 39870 osumcllem4N 39961 pexmidlem1N 39972 lhp2lt 40003 lhp2atne 40036 lhp2at0ne 40038 4atexlemunv 40068 4atexlemex2 40073 trlne 40187 trlval4 40190 cdlemc4 40196 cdleme11dN 40264 cdleme11h 40268 cdlemednuN 40302 cdleme20j 40320 cdleme20k 40321 cdleme21at 40330 cdleme35f 40456 cdlemg11b 40644 dia2dimlem1 41066 dihmeetlem3N 41307 dihmeetlem15N 41323 dochsnnz 41452 dochexmidlem1 41462 dochexmidlem7 41468 mapdindp3 41724 fltne 42654 pellexlem1 42840 dfac21 43078 pm13.14 44428 uzlidlring 48151 suppdm 48427 |
| Copyright terms: Public domain | W3C validator |