theorem :: INTPRO_2:165

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