Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > necomd | Unicode version |
Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.) |
Ref | Expression |
---|---|
necomd.1 |
Ref | Expression |
---|---|
necomd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | necomd.1 | . 2 | |
2 | necom 2411 | . 2 | |
3 | 1, 2 | sylib 121 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wne 2327 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-5 1427 ax-gen 1429 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-cleq 2150 df-ne 2328 |
This theorem is referenced by: difsnb 3700 0nelop 4209 frecabcl 6347 fidifsnen 6816 tpfidisj 6873 omp1eomlem 7039 difinfsnlem 7044 fodjuomnilemdc 7088 en2eleq 7131 en2other2 7132 ltned 7991 lt0ne0 8304 zdceq 9240 zneo 9266 xrlttri3 9705 qdceq 10150 flqltnz 10190 nn0opthd 10600 hashdifpr 10698 sumtp 11315 isprm2lem 11997 oddprm 12138 ennnfonelemex 12185 |
Copyright terms: Public domain | W3C validator |