theorem Th47: :: INTPRO_2:46

for p being Element of MC-wff holds FALSUM => p is valid_IPC