theorem Th22: :: INTPRO_2:21

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC p => (q => (p '&' q)) by INTPRO_1:5;