theorem Th57: :: INTPRO_2:56

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