theorem :: INTPRO_1:77

IPC-Taut c= CPC-Taut by Th68;