theorem Th69: :: INTPRO_2:68

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