theorem Th37: :: INTPRO_1:37
for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p '&' q) => r) in IPC-Taut