theorem :: HILBERT1:28

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