theorem Th45: :: INTPRO_1:45

for p, q, s being Element of MC-wff holds ((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut