![]() |
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 2431 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 122 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-5 1447 ax-gen 1449 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-ne 2348 |
This theorem is referenced by: difsnb 3734 0nelop 4244 frecabcl 6393 fidifsnen 6863 tpfidisj 6920 omp1eomlem 7086 difinfsnlem 7091 fodjuomnilemdc 7135 en2eleq 7187 en2other2 7188 ltned 8048 lt0ne0 8362 zdceq 9304 zneo 9330 xrlttri3 9771 qdceq 10220 flqltnz 10260 nn0opthd 10673 hashdifpr 10771 sumtp 11393 isprm2lem 12086 oddprm 12229 pcmpt 12311 ennnfonelemex 12385 lgsneg 14058 |
Copyright terms: Public domain | W3C validator |