theorem :: INTPRO_2:153

for p being Element of MC-wff holds |-_IPC (neg p) 'equiv' (neg (neg (neg p))) by Th104;