theorem Th40: :: HILBERT1:40

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