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