theorem Th32: :: INTPRO_2:31

for p, q being Element of MC-wff holds |-_IPC p => (q => (p '&' q)) by Th22;