theorem :: HILBERT1:37

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