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 3023 | 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: r19.2zb 4439 pwne 5243 onnev 6305 alephord 9490 ackbij1lem18 9648 fin23lem26 9736 fin1a2lem6 9816 alephom 9996 gchxpidm 10080 egt2lt3 15549 nn0onn 15721 prmodvdslcmf 16373 symgfix2 18475 alexsubALTlem2 22586 alexsubALTlem4 22588 ptcmplem2 22591 nmoid 23280 cxplogb 25291 axlowdimlem17 26672 frgrncvvdeq 28016 hashxpe 30456 hasheuni 31244 limsucncmpi 33691 matunitlindflem1 34770 poimirlem32 34806 ovoliunnfl 34816 voliunnfl 34818 volsupnfl 34819 dvasin 34860 lsat0cv 36051 pellexlem5 39310 uzfissfz 41474 xralrple2 41502 infxr 41515 icccncfext 42050 ioodvbdlimc1lem1 42096 volioc 42137 fourierdlem32 42305 fourierdlem49 42321 fourierdlem73 42345 fourierswlem 42396 fouriersw 42397 sge0pr 42557 voliunsge0lem 42635 carageniuncl 42686 isomenndlem 42693 hoimbl 42794 |
Copyright terms: Public domain | W3C validator |