theorem Th46: :: INTPRO_1:46

for p, q being Element of MC-wff holds (p '&' q) => (q '&' p) in IPC-Taut