theorem Th39: :: MODAL_1:44
for A, B, C being MP-wff holds
( 'not' A <> (#) B & 'not' A <> B '&' C )