theorem :: INTPRO_2:152

for p being Element of MC-wff holds |-_IPC (neg (neg (neg p))) => (neg p) by Th103;