let p, q, r be Element of CQC-WFF ; :: thesis: ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT
A1: (('not' p) 'or' (('not' r) 'or' ('not' q))) => ((('not' r) 'or' ('not' q)) 'or' ('not' p)) in TAUT by Th8;
( ('not' (q '&' r)) => (('not' q) 'or' ('not' r)) in TAUT & (('not' q) 'or' ('not' r)) => (('not' r) 'or' ('not' q)) in TAUT ) by Th8, Th17;
then ('not' (q '&' r)) => (('not' r) 'or' ('not' q)) in TAUT by LUKASI_1:3;
then A2: ('not' ('not' p)) => (('not' (q '&' r)) => (('not' r) 'or' ('not' q))) in TAUT by LUKASI_1:13;
(('not' ('not' p)) => (('not' (q '&' r)) => (('not' r) 'or' ('not' q)))) => ((('not' ('not' p)) => ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q)))) in TAUT by LUKASI_1:11;
then (('not' ('not' p)) => ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q))) in TAUT by A2, CQC_THE1:46;
then (('not' p) 'or' ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q))) in TAUT by Lm1;
then A3: (('not' p) 'or' ('not' (q '&' r))) => (('not' p) 'or' (('not' r) 'or' ('not' q))) in TAUT by Lm1;
('not' (p '&' (q '&' r))) => (('not' p) 'or' ('not' (q '&' r))) in TAUT by Th17;
then ('not' (p '&' (q '&' r))) => (('not' p) 'or' (('not' r) 'or' ('not' q))) in TAUT by A3, LUKASI_1:3;
then A4: ('not' (p '&' (q '&' r))) => ((('not' r) 'or' ('not' q)) 'or' ('not' p)) in TAUT by A1, LUKASI_1:3;
A5: (('not' (p '&' q)) 'or' ('not' r)) => ('not' ((p '&' q) '&' r)) in TAUT by Th18;
( (('not' q) 'or' ('not' p)) => (('not' p) 'or' ('not' q)) in TAUT & (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT ) by Th8, Th18;
then (('not' q) 'or' ('not' p)) => ('not' (p '&' q)) in TAUT by LUKASI_1:3;
then A6: ('not' ('not' r)) => ((('not' q) 'or' ('not' p)) => ('not' (p '&' q))) in TAUT by LUKASI_1:13;
(('not' ('not' r)) => ((('not' q) 'or' ('not' p)) => ('not' (p '&' q)))) => ((('not' ('not' r)) => (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q)))) in TAUT by LUKASI_1:11;
then (('not' ('not' r)) => (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q))) in TAUT by A6, CQC_THE1:46;
then (('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q))) in TAUT by Lm1;
then A7: (('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' r) 'or' ('not' (p '&' q))) in TAUT by Lm1;
(('not' r) 'or' ('not' (p '&' q))) => (('not' (p '&' q)) 'or' ('not' r)) in TAUT by Th8;
then (('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' (p '&' q)) 'or' ('not' r)) in TAUT by A7, LUKASI_1:3;
then A8: (('not' r) 'or' (('not' q) 'or' ('not' p))) => ('not' ((p '&' q) '&' r)) in TAUT by A5, LUKASI_1:3;
((('not' r) 'or' ('not' q)) 'or' ('not' p)) => (('not' r) 'or' (('not' q) 'or' ('not' p))) in TAUT by Th25;
then ('not' (p '&' (q '&' r))) => (('not' r) 'or' (('not' q) 'or' ('not' p))) in TAUT by A4, LUKASI_1:3;
then ('not' (p '&' (q '&' r))) => ('not' ((p '&' q) '&' r)) in TAUT by A8, LUKASI_1:3;
hence ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT by LUKASI_1:35; :: thesis: verum