theorem Th21: :: HILBERT1:21

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