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