theorem Th23: :: HILBERT1:23

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