theorem :: INTPRO_2:166

for p, q, r being Element of MC-wff holds |-_IPC (p => q) => ((neg (q 'or' r)) => (neg (p 'or' r))) by Th128;