let p, q, r be Element of PL-WFF ; :: thesis: ((p '&' q) '&' r) <=> (p '&' (q '&' r)) is tautology
let M be PLModel; :: according to PL_AXIOM:def 18 :: thesis: (SAT M) . (((p '&' q) '&' r) <=> (p '&' (q '&' r))) = 1
thus (SAT M) . (((p '&' q) '&' r) <=> (p '&' (q '&' r))) = ((SAT M) . ((p '&' q) '&' r)) <=> ((SAT M) . (p '&' (q '&' r))) by semequ2
.= (((SAT M) . (p '&' q)) '&' ((SAT M) . r)) <=> ((SAT M) . (p '&' (q '&' r))) by semcon2
.= (((SAT M) . (p '&' q)) '&' ((SAT M) . r)) <=> (((SAT M) . p) '&' ((SAT M) . (q '&' r))) by semcon2
.= (((SAT M) . (p '&' q)) '&' ((SAT M) . r)) <=> (((SAT M) . p) '&' (((SAT M) . q) '&' ((SAT M) . r))) by semcon2
.= ((((SAT M) . p) '&' ((SAT M) . q)) '&' ((SAT M) . r)) <=> (((SAT M) . p) '&' (((SAT M) . q) '&' ((SAT M) . r))) by semcon2
.= 1 by th7 ; :: thesis: verum