theorem Th26: :: HILBERT1:26

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