![]() |
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 2191 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | necon3bii 2398 |
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 615 ax-in2 616 ax-5 1458 ax-gen 1460 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-ne 2361 |
This theorem is referenced by: necomi 2445 necomd 2446 difprsn1 3746 difprsn2 3747 diftpsn3 3748 fndmdifcom 5643 fvpr1 5741 fvpr2 5742 fvpr1g 5743 fvtp1g 5745 fvtp2g 5746 fvtp3g 5747 fvtp2 5749 fvtp3 5750 netap 7283 2omotaplemap 7286 zltlen 9361 nn0lt2 9364 qltlen 9670 fzofzim 10218 flqeqceilz 10349 isprm2lem 12148 prm2orodd 12158 tridceq 15266 |
Copyright terms: Public domain | W3C validator |