theorem :: INTPRO_2:85

for p being Element of MC-wff holds |-_IPC p 'equiv' p