theorem Th27: :: HILBERT1:27

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