![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ancomd | Unicode version |
Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.) |
Ref | Expression |
---|---|
ancomd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ancomd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancomd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ancom 266 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 122 |
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 |
This theorem is referenced by: elres 4964 relbrcnvg 5028 fvelrnb 5587 relelec 6605 prcdnql 7518 1idpru 7625 gt0srpr 7782 fihashf1rn 10809 prodmodclem3 11624 sinbnd 11801 cosbnd 11802 dvdsdivcl 11897 nn0ehalf 11949 nn0oddm1d2 11955 nnoddm1d2 11956 coprmgcdb 12131 divgcdcoprm0 12144 divgcdcoprmex 12145 cncongr1 12146 quscrng 13872 sincosq2sgn 14733 sincosq4sgn 14735 |
Copyright terms: Public domain | W3C validator |