theorem Th84: :: INTPRO_2:83

for p, q being Element of MC-wff st |-_IPC p => q & |-_IPC q => p holds
|-_IPC p 'equiv' q by Th83;