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 264 | . 2 | |
3 | 1, 2 | sylib 121 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: elres 4855 relbrcnvg 4918 fvelrnb 5469 relelec 6469 prcdnql 7292 1idpru 7399 gt0srpr 7556 focdmex 10533 fihashf1rn 10535 prodmodclem3 11344 sinbnd 11459 cosbnd 11460 dvdsdivcl 11548 nn0ehalf 11600 nn0oddm1d2 11606 nnoddm1d2 11607 coprmgcdb 11769 divgcdcoprm0 11782 divgcdcoprmex 11783 cncongr1 11784 sincosq2sgn 12908 sincosq4sgn 12910 |
Copyright terms: Public domain | W3C validator |