theorem Th55: :: INTPRO_2:54

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