theorem :: INTPRO_2:117

for p, q, r being Element of MC-wff st |-_IPC p & {r} |-_IPC q holds
{(p => r)} |-_IPC q