theorem Th19: :: HILBERT1:19

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