![]() |
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 142 | . 2 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
2 | necon2ad.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) | |
3 | 2 | necon3bd 2954 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 ≠ 𝐵)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ 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 206 df-ne 2941 |
This theorem is referenced by: necon2d 2963 prneimg 4813 tz7.2 5618 nordeq 6337 xpord3inddlem 8087 omxpenlem 9020 pr2neOLD 9946 cflim2 10204 cfslb2n 10209 ltne 11257 sqrt2irr 16136 rpexp 16603 pcgcd1 16754 plttr 18236 odhash3 19363 lbspss 20558 nzrunit 20753 en2top 22351 fbfinnfr 23208 ufileu 23286 alexsubALTlem4 23417 lebnumlem1 24340 lebnumlem2 24341 lebnumlem3 24342 ivthlem2 24832 ivthlem3 24833 dvne0 25391 deg1nn0clb 25471 lgsmod 26687 nodenselem4 27051 nodenselem5 27052 nodenselem7 27054 noinfbnd2lem1 27094 slerec 27180 addsval 27296 axlowdimlem16 27948 upgrewlkle2 28596 wlkon2n0 28656 pthdivtx 28719 normgt0 30111 pmtrcnel 31989 lindsadd 36117 poimirlem16 36140 poimirlem17 36141 poimirlem19 36143 poimirlem21 36145 poimirlem27 36151 islln2a 38026 islpln2a 38057 islvol2aN 38101 dalem1 38168 trlnidatb 38686 ensucne0OLD 41890 lswn0 45722 nnsum4primeseven 46078 nnsum4primesevenALTV 46079 dignn0flhalflem1 46787 |
Copyright terms: Public domain | W3C validator |