theorem :: HILBERT1:38

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