:: deftheorem defines valid_IPC INTPRO_2:def 8 :
for s being MC-formula holds
( s is valid_IPC iff {} MC-wff |-_IPC s );