theorem Th43: :: INTPRO_2:42

for p, q being Element of MC-wff holds p => (q => (p '&' q)) is valid_IPC