theorem :: HILBERT1:17

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