let F1, F2, F3, F4, F5, F6, F7, G be MC-formula; ( {F1,F2,F3,F4,F5,F6,F7} |-_IPC G implies {F2,F3,F4,F5,F6,F7} |-_IPC F1 => G )
{F1,F2,F3,F4,F5,F6,F7} = {F2,F3,F4,F5,F6,F7} \/ {F1}
by ENUMSET1:16;
hence
( {F1,F2,F3,F4,F5,F6,F7} |-_IPC G implies {F2,F3,F4,F5,F6,F7} |-_IPC F1 => G )
by Th53; verum