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