theorem Th36: :: HILBERT1:36

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