theorem Th70: :: INTPRO_2:69

for p being Element of MC-wff st |-_IPC p holds
p in IPC-Taut by Def6, INTPRO_1:def 16;