theorem Th54: :: INTPRO_2:53

for F being Element of MC-wff
for G being MC-formula st {F} |-_IPC G holds
|-_IPC F => G