theorem Th30: :: HILBERT1:30

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