![]() |
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 2944 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 ≠ 𝐵)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1534 ≠ wne 2930 |
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 2931 |
This theorem is referenced by: necon2d 2953 prneimg 4853 tz7.2 5656 nordeq 6384 xpord3inddlem 8157 omxpenlem 9100 pr2neOLD 10038 cflim2 10294 cfslb2n 10299 ltne 11349 sqrt2irr 16243 rpexp 16716 pcgcd1 16871 plttr 18359 odhash3 19567 nzrunit 20499 lbspss 21053 en2top 22973 fbfinnfr 23830 ufileu 23908 alexsubALTlem4 24039 lebnumlem1 24972 lebnumlem2 24973 lebnumlem3 24974 ivthlem2 25466 ivthlem3 25467 dvne0 26029 deg1nn0clb 26111 lgsmod 27346 nodenselem4 27711 nodenselem5 27712 nodenselem7 27714 noinfbnd2lem1 27754 sltne 27794 slerec 27843 cuteq1 27857 addsval 27970 axlowdimlem16 28885 upgrewlkle2 29537 wlkon2n0 29597 pthdivtx 29660 normgt0 31054 pmtrcnel 32968 lindsadd 37324 poimirlem16 37347 poimirlem17 37348 poimirlem19 37350 poimirlem21 37352 poimirlem27 37358 islln2a 39226 islpln2a 39257 islvol2aN 39301 dalem1 39368 trlnidatb 39886 ensucne0OLD 43231 lswn0 47049 nnsum4primeseven 47405 nnsum4primesevenALTV 47406 dignn0flhalflem1 48036 |
Copyright terms: Public domain | W3C validator |