theorem :: INTPRO_1:31

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