theorem Th32: :: INTPRO_1:32

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