theorem Th30: :: INTPRO_1:30

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