let q, r be Element of MC-wff ; :: thesis: ( |-_IPC r & {r} |-_IPC q implies |-_IPC q )
assume A1: ( |-_IPC r & {r} |-_IPC q ) ; :: thesis: |-_IPC q
then |-_IPC r => q by Th54;
hence |-_IPC q by A1, Th37; :: thesis: verum