Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > necom | Unicode version |
Description: Commutation of inequality. (Contributed by NM, 14-May-1999.) |
Ref | Expression |
---|---|
necom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom 2119 | . 2 | |
2 | 1 | necon3bii 2323 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wne 2285 |
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 588 ax-in2 589 ax-5 1408 ax-gen 1410 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 df-ne 2286 |
This theorem is referenced by: necomi 2370 necomd 2371 difprsn1 3629 difprsn2 3630 diftpsn3 3631 fndmdifcom 5494 fvpr1 5592 fvpr2 5593 fvpr1g 5594 fvtp1g 5596 fvtp2g 5597 fvtp3g 5598 fvtp2 5600 fvtp3 5601 zltlen 9097 nn0lt2 9100 qltlen 9400 fzofzim 9933 flqeqceilz 10059 isprm2lem 11724 prm2orodd 11734 |
Copyright terms: Public domain | W3C validator |