theorem Th28: :: INTPRO_2:27

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