theorem Th56: :: INTPRO_2:55

for F1, F2, F3, G being MC-formula st {F1,F2,F3} |-_IPC G holds
{F2,F3} |-_IPC F1 => G