![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > necon2ad | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.) |
Ref | Expression |
---|---|
necon2ad.1 | ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
Ref | Expression |
---|---|
necon2ad | ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnot 139 | . 2 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
2 | necon2ad.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) | |
3 | 2 | necon3bd 2975 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 ≠ 𝐵)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1507 ≠ wne 2961 |
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 2962 |
This theorem is referenced by: necon2d 2984 prneimg 4653 tz7.2 5385 nordeq 6042 omxpenlem 8408 pr2ne 9219 cflim2 9477 cfslb2n 9482 ltne 10531 sqrt2irr 15456 rpexp 15914 pcgcd1 16063 plttr 17432 odhash3 18456 lbspss 19570 nzrunit 19755 en2top 21291 fbfinnfr 22147 ufileu 22225 alexsubALTlem4 22356 lebnumlem1 23262 lebnumlem2 23263 lebnumlem3 23264 ivthlem2 23750 ivthlem3 23751 dvne0 24305 deg1nn0clb 24381 lgsmod 25595 axlowdimlem16 26440 upgrewlkle2 27085 wlkon2n0 27144 pthdivtx 27212 normgt0 28677 nodenselem4 32712 nodenselem5 32713 nodenselem7 32715 slerec 32798 lindsadd 34326 poimirlem16 34349 poimirlem17 34350 poimirlem19 34352 poimirlem21 34354 poimirlem27 34360 islln2a 36098 islpln2a 36129 islvol2aN 36173 dalem1 36240 trlnidatb 36758 lswn0 42976 nnsum4primeseven 43333 nnsum4primesevenALTV 43334 dignn0flhalflem1 44043 |
Copyright terms: Public domain | W3C validator |