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 150 | . 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵) |
3 | 2 | neqned 2801 | 1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1483 ≠ wne 2794 |
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 2795 |
This theorem is referenced by: r19.2zb 4061 pwne 4831 onnev 5848 alephord 8898 ackbij1lem18 9059 fin23lem26 9147 fin1a2lem6 9227 alephom 9407 gchxpidm 9491 egt2lt3 14934 prmodvdslcmf 15751 symgfix2 17836 chfacfisf 20659 chfacfisfcpmat 20660 alexsubALTlem2 21852 alexsubALTlem4 21854 ptcmplem2 21857 nmoid 22546 cxplogb 24524 axlowdimlem17 25838 frgrncvvdeq 27173 hasheuni 30147 limsucncmpi 32444 matunitlindflem1 33405 poimirlem32 33441 ovoliunnfl 33451 voliunnfl 33453 volsupnfl 33454 dvasin 33496 lsat0cv 34320 pellexlem5 37397 uzfissfz 39542 xralrple2 39570 infxr 39583 icccncfext 40100 ioodvbdlimc1lem1 40146 volioc 40188 fourierdlem32 40356 fourierdlem49 40372 fourierdlem73 40396 fourierswlem 40447 fouriersw 40448 prsal 40538 sge0pr 40611 voliunsge0lem 40689 carageniuncl 40737 isomenndlem 40744 hoimbl 40845 |
Copyright terms: Public domain | W3C validator |