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 2172 | . 2 | |
2 | 1 | necon3bii 2378 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wne 2340 |
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 609 ax-in2 610 ax-5 1440 ax-gen 1442 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-ne 2341 |
This theorem is referenced by: necomi 2425 necomd 2426 difprsn1 3719 difprsn2 3720 diftpsn3 3721 fndmdifcom 5602 fvpr1 5700 fvpr2 5701 fvpr1g 5702 fvtp1g 5704 fvtp2g 5705 fvtp3g 5706 fvtp2 5708 fvtp3 5709 zltlen 9290 nn0lt2 9293 qltlen 9599 fzofzim 10144 flqeqceilz 10274 isprm2lem 12070 prm2orodd 12080 tridceq 14088 |
Copyright terms: Public domain | W3C validator |