theorem :: INTPRO_2:61

for F1, F2, F3, F4, F5, F6, F7, F8, F9, G being MC-formula st {F1,F2,F3,F4,F5,F6,F7,F8,F9} |-_IPC G holds
{F2,F3,F4,F5,F6,F7,F8,F9} |-_IPC F1 => G