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 3717 difprsn2 3718 diftpsn3 3719 fndmdifcom 5599 fvpr1 5697 fvpr2 5698 fvpr1g 5699 fvtp1g 5701 fvtp2g 5702 fvtp3g 5703 fvtp2 5705 fvtp3 5706 zltlen 9277 nn0lt2 9280 qltlen 9586 fzofzim 10131 flqeqceilz 10261 isprm2lem 12057 prm2orodd 12067 tridceq 14048 |
Copyright terms: Public domain | W3C validator |