![]() |
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 263 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylib 121 |
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 |
This theorem is referenced by: elres 4763 relbrcnvg 4826 fvelrnb 5367 relelec 6348 prcdnql 7106 1idpru 7213 gt0srpr 7357 focdmex 10258 fihashf1rn 10260 sinbnd 11106 cosbnd 11107 dvdsdivcl 11192 nn0ehalf 11244 nn0oddm1d2 11250 nnoddm1d2 11251 coprmgcdb 11411 divgcdcoprm0 11424 divgcdcoprmex 11425 cncongr1 11426 |
Copyright terms: Public domain | W3C validator |