![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3coml | Unicode version |
Description: Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.) |
Ref | Expression |
---|---|
3exp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3coml |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3com23 1170 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3com13 1169 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: 3comr 1172 nndir 6340 f1oen2g 6603 f1dom2g 6604 ordiso 6873 addassnqg 7138 ltbtwnnqq 7171 nnanq0 7214 ltasrg 7513 recexgt0sr 7516 axmulass 7608 adddir 7681 axltadd 7758 ltleletr 7769 letr 7770 pnpcan2 7925 subdir 8067 div13ap 8366 zdiv 9043 xrletr 9484 fzen 9716 fzrevral2 9779 fzshftral 9781 fzind2 9909 mulbinom2 10301 elicc4abs 10758 dvdsnegb 11358 muldvds1 11366 muldvds2 11367 dvdscmul 11368 dvdsmulc 11369 dvdsgcd 11546 mulgcdr 11552 lcmgcdeq 11610 congr 11627 mettri 12362 cnmet 12519 addcncntoplem 12537 |
Copyright terms: Public domain | W3C validator |