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