theorem Th22: :: HILBERT1:22

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