theorem :: INTPRO_2:141

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