theorem Th20: :: HILBERT1:20

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