let F1, F2, G be MC-formula; :: thesis: ( {F1,F2} |-_IPC G implies {F2} |-_IPC F1 => G )
{F1,F2} = {F2} \/ {F1} by ENUMSET1:1;
hence ( {F1,F2} |-_IPC G implies {F2} |-_IPC F1 => G ) by Th53; :: thesis: verum