theorem Th29: :: HILBERT1:29

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