theorem :: INTPRO_2:70

for p being Element of MC-wff holds
( p in IPC-Taut iff |-_IPC p ) by Th69, Th70;