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 144 | . 2 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
2 | necon2ad.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) | |
3 | 2 | necon3bd 3030 | . 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 ≠ 𝐵)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ≠ wne 3016 |
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 208 df-ne 3017 |
This theorem is referenced by: necon2d 3039 prneimg 4779 tz7.2 5533 nordeq 6204 omxpenlem 8607 pr2ne 9420 cflim2 9674 cfslb2n 9679 ltne 10726 sqrt2irr 15592 rpexp 16054 pcgcd1 16203 plttr 17570 odhash3 18632 lbspss 19785 nzrunit 19970 en2top 21523 fbfinnfr 22379 ufileu 22457 alexsubALTlem4 22588 lebnumlem1 23494 lebnumlem2 23495 lebnumlem3 23496 ivthlem2 23982 ivthlem3 23983 dvne0 24537 deg1nn0clb 24613 lgsmod 25827 axlowdimlem16 26671 upgrewlkle2 27316 wlkon2n0 27376 pthdivtx 27438 normgt0 28832 pmtrcnel 30661 nodenselem4 33089 nodenselem5 33090 nodenselem7 33092 slerec 33175 lindsadd 34767 poimirlem16 34790 poimirlem17 34791 poimirlem19 34793 poimirlem21 34795 poimirlem27 34801 islln2a 36535 islpln2a 36566 islvol2aN 36610 dalem1 36677 trlnidatb 37195 ensucne0OLD 39776 lswn0 43451 nnsum4primeseven 43812 nnsum4primesevenALTV 43813 dignn0flhalflem1 44573 |
Copyright terms: Public domain | W3C validator |