theorem Th42: :: INTPRO_1:42

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