theorem :: INTPRO_2:47

for p, q being Element of MC-wff st p is valid_IPC & p => q is valid_IPC holds
q is valid_IPC