theorem Th30: :: MODAL_1:35

for A, A1, B, B1 being MP-wff st A '&' B = A1 '&' B1 holds
( A = A1 & B = B1 )