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