theorem Th46: :: HILBERT1:46

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