![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neneq | Structured version Visualization version GIF version |
Description: From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
neneq | ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵) | |
2 | 1 | neneqd 2946 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ wne 2941 |
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 2942 |
This theorem is referenced by: necon3ad 2954 necon3ai 2966 2reu4lem 4521 pr1eqbg 4853 disjprgw 5139 fpropnf1 7253 nf1const 7289 nelaneq 9581 gcd2n0cl 16437 lcmfunsnlem2lem1 16562 lcmfunsnlem2lem2 16563 ncoprmgcdne1b 16574 isnsgrp 18601 isnmnd 18616 mulmarep1gsum1 22044 fvmptnn04ifb 22322 tdeglem4 25546 isosctrlem2 26291 structiedg0val 28249 umgr2edgneu 28438 imadifxp 31798 f1resrcmplf1dlem 34020 aks6d1c2p2 40863 xppss12 40963 n0p 43601 supxrge 43921 uzn0bi 44042 elprn1 44222 elprn2 44223 liminflbuz2 44404 itgcoscmulx 44558 fourierdlem41 44737 elaa2 44823 sge0cl 44970 meadjiunlem 45054 hoidmvlelem2 45185 hspmbllem1 45215 |
Copyright terms: Public domain | W3C validator |