theorem :: HILBERT1:25

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