let p, q, r be Element of CQC-WFF ; :: thesis: ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT
A1: ('not' (p '&' (q '&' r))) => (('not' p) 'or' ('not' (q '&' r))) in TAUT by Th17;
A2: ('not' (q '&' r)) => (('not' q) 'or' ('not' r)) in TAUT by Th17;
(('not' q) 'or' ('not' r)) => (('not' r) 'or' ('not' q)) in TAUT by Th8;
then ('not' (q '&' r)) => (('not' r) 'or' ('not' q)) in TAUT by A2, LUKASI_1:3;
then A3: ('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 A3, CQC_THE1:82;
then (('not' p) 'or' ('not' (q '&' r))) => (('not' ('not' p)) => (('not' r) 'or' ('not' q))) in TAUT by Lm1;
then (('not' p) 'or' ('not' (q '&' r))) => (('not' p) 'or' (('not' r) 'or' ('not' q))) in TAUT by Lm1;
then A4: ('not' (p '&' (q '&' r))) => (('not' p) 'or' (('not' r) 'or' ('not' q))) in TAUT by A1, LUKASI_1:3;
(('not' p) 'or' (('not' r) 'or' ('not' q))) => ((('not' r) 'or' ('not' q)) 'or' ('not' p)) in TAUT by Th8;
then A5: ('not' (p '&' (q '&' r))) => ((('not' r) 'or' ('not' q)) 'or' ('not' p)) in TAUT by A4, LUKASI_1:3;
((('not' r) 'or' ('not' q)) 'or' ('not' p)) => (('not' r) 'or' (('not' q) 'or' ('not' p))) in TAUT by Th25;
then A6: ('not' (p '&' (q '&' r))) => (('not' r) 'or' (('not' q) 'or' ('not' p))) in TAUT by A5, LUKASI_1:3;
A7: (('not' q) 'or' ('not' p)) => (('not' p) 'or' ('not' q)) in TAUT by Th8;
(('not' p) 'or' ('not' q)) => ('not' (p '&' q)) in TAUT by Th18;
then (('not' q) 'or' ('not' p)) => ('not' (p '&' q)) in TAUT by A7, LUKASI_1:3;
then A8: ('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 A8, CQC_THE1:82;
then (('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' ('not' r)) => ('not' (p '&' q))) in TAUT by Lm1;
then A9: (('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 A10: (('not' r) 'or' (('not' q) 'or' ('not' p))) => (('not' (p '&' q)) 'or' ('not' r)) in TAUT by A9, LUKASI_1:3;
(('not' (p '&' q)) 'or' ('not' r)) => ('not' ((p '&' q) '&' r)) in TAUT by Th18;
then (('not' r) 'or' (('not' q) 'or' ('not' p))) => ('not' ((p '&' q) '&' r)) in TAUT by A10, LUKASI_1:3;
then ('not' (p '&' (q '&' r))) => ('not' ((p '&' q) '&' r)) in TAUT by A6, LUKASI_1:3;
hence ((p '&' q) '&' r) => (p '&' (q '&' r)) in TAUT by LUKASI_1:35; :: thesis: verum