let p, q, r be Element of MC-wff ; :: thesis: ( |-_IPC p & {r} |-_IPC q implies {(p => r)} |-_IPC q )
A20: {} c= {(p => r)} ;
assume A1: ( |-_IPC p & {r} |-_IPC q ) ; :: thesis: {(p => r)} |-_IPC q
then A2: {(p => r)} |-_IPC p by A20, Th66;
{(p => r)} |-_IPC p => r by Th65;
then A4: {(p => r)} |-_IPC r by A2, Th27;
{r} c= {(p => r)} \/ {r} by XBOOLE_1:7;
then {(p => r)} \/ {r} |-_IPC q by A1, Th66;
hence {(p => r)} |-_IPC q by A4, Th116; :: thesis: verum