theorem Th34: :: HILBERT1:34

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