| 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 2961 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1559 ≠ wne 2956 |
| 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 209 df-ne 2957 |
| This theorem is referenced by: necon3ad 2969 necon3ai 2981 2reu4lem 4476 elprn1 4609 elprn2 4610 pr1eqbg 4814 fpropnf1 7245 nf1const 7282 nelaneqOLDOLD 9547 gcd2n0cl 16524 lcmfunsnlem2lem1 16653 lcmfunsnlem2lem2 16654 ncoprmgcdne1b 16665 isnsgrp 18738 isnmnd 18753 mulmarep1gsum1 22611 fvmptnn04ifb 22889 tdeglem4 26098 isosctrlem2 26859 nnsge1 28411 structiedg0val 29167 umgr2edgneu 29359 imadifxp 32748 f1resrcmplf1dlem 35342 elttcirr 36844 aks6d1c2p2 42689 xppss12 42801 n0p 45578 supxrge 45867 uzn0bi 45986 liminflbuz2 46342 itgcoscmulx 46496 fourierdlem41 46675 elaa2 46761 sge0cl 46908 meadjiunlem 46992 hoidmvlelem2 47123 hspmbllem1 47153 chnerlem1 47411 |
| Copyright terms: Public domain | W3C validator |