Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > necon3bi | Structured version Visualization version GIF version |
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.) |
Ref | Expression |
---|---|
necon3bi.1 | ⊢ (𝐴 = 𝐵 → 𝜑) |
Ref | Expression |
---|---|
necon3bi | ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necon3bi.1 | . . 3 ⊢ (𝐴 = 𝐵 → 𝜑) | |
2 | 1 | con3i 157 | . 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 2941 | 1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ wne 2934 |
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 210 df-ne 2935 |
This theorem is referenced by: r19.2zb 4382 pwne 5217 onnevOLD 6294 alephord 9575 ackbij1lem18 9737 fin23lem26 9825 fin1a2lem6 9905 alephom 10085 gchxpidm 10169 egt2lt3 15651 nn0onn 15825 prmodvdslcmf 16483 symgfix2 18662 alexsubALTlem2 22799 alexsubALTlem4 22801 ptcmplem2 22804 nmoid 23495 cxplogb 25524 axlowdimlem17 26904 frgrncvvdeq 28246 hashxpe 30702 hasheuni 31623 limsucncmpi 34272 matunitlindflem1 35396 poimirlem32 35432 ovoliunnfl 35442 voliunnfl 35444 volsupnfl 35445 dvasin 35484 lsat0cv 36670 metakunt24 39739 pellexlem5 40227 uzfissfz 42403 xralrple2 42431 infxr 42444 icccncfext 42970 ioodvbdlimc1lem1 43014 volioc 43055 fourierdlem32 43222 fourierdlem49 43238 fourierdlem73 43262 fourierswlem 43313 fouriersw 43314 sge0pr 43474 voliunsge0lem 43552 carageniuncl 43603 isomenndlem 43610 hoimbl 43711 |
Copyright terms: Public domain | W3C validator |