theorem Th27: :: INTPRO_1:27

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