let F be Element of MC-wff ; :: thesis: for G being MC-formula st {F} |-_IPC G holds
|-_IPC F => G
let G be MC-formula; :: thesis: ( {F} |-_IPC G implies |-_IPC F => G )
{F} = {F} \/ ({} MC-wff) ;
hence ( {F} |-_IPC G implies |-_IPC F => G ) by Th53; :: thesis: verum