![]() |
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 1211 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3com13 1210 |
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 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: 3comr 1213 nndir 6516 f1oen2g 6782 f1dom2g 6783 ordiso 7066 addassnqg 7412 ltbtwnnqq 7445 nnanq0 7488 ltasrg 7800 recexgt0sr 7803 axmulass 7903 adddir 7979 axltadd 8058 ltleletr 8070 letr 8071 pnpcan2 8228 subdir 8374 div13ap 8681 zdiv 9372 xrletr 9840 fzen 10075 fzrevral2 10138 fzshftral 10140 fzind2 10271 mulbinom2 10671 elicc4abs 11138 dvdsnegb 11850 muldvds1 11858 muldvds2 11859 dvdscmul 11860 dvdsmulc 11861 dvdsgcd 12048 mulgcdr 12054 lcmgcdeq 12118 congr 12135 mulgnnass 13114 mettri 14350 cnmet 14507 addcncntoplem 14528 |
Copyright terms: Public domain | W3C validator |