theorem Th24: :: HILBERT1:24

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