theorem Th61: :: INTPRO_1:61

for p, q, s being Element of MC-wff st p => q in IPC-Taut holds
(p 'or' s) => (q 'or' s) in IPC-Taut