theorem Th43: :: HILBERT1:43

for p, q being Element of HP-WFF holds (p '&' q) => (q '&' p) in HP_TAUT