![]() |
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 136 | . 2 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
2 | necon2ad.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) | |
3 | 2 | necon3bd 2837 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 ≠ 𝐵)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1523 ≠ wne 2823 |
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 197 df-ne 2824 |
This theorem is referenced by: necon2d 2846 prneimg 4419 tz7.2 5127 nordeq 5780 omxpenlem 8102 pr2ne 8866 cflim2 9123 cfslb2n 9128 ltne 10172 sqrt2irr 15023 rpexp 15479 pcgcd1 15628 plttr 17017 odhash3 18037 lbspss 19130 nzrunit 19315 en2top 20837 fbfinnfr 21692 ufileu 21770 alexsubALTlem4 21901 lebnumlem1 22807 lebnumlem2 22808 lebnumlem3 22809 ivthlem2 23267 ivthlem3 23268 dvne0 23819 deg1nn0clb 23895 lgsmod 25093 axlowdimlem16 25882 upgrewlkle2 26558 wlkon2n0 26618 pthdivtx 26681 normgt0 28112 nodenselem4 31962 nodenselem5 31963 nodenselem7 31965 slerec 32048 poimirlem16 33555 poimirlem17 33556 poimirlem19 33558 poimirlem21 33560 poimirlem27 33566 islln2a 35121 islpln2a 35152 islvol2aN 35196 dalem1 35263 trlnidatb 35782 lswn0 41705 nnsum4primeseven 42013 nnsum4primesevenALTV 42014 dignn0flhalflem1 42734 |
Copyright terms: Public domain | W3C validator |