theorem Th18: :: INTPRO_2:17

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