let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A holds (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A
let p, q, r be Element of CQC-WFF A; :: thesis: (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A
set AA = ('not' r) => ('not' p);
set B = ('not' r) => ('not' q);
set C = ('not' r) => (('not' p) '&' ('not' q));
set D = (p 'or' q) => r;
set E = q => r;
A1: (('not' r) => ('not' p)) => ((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) in TAUT A by Th33;
(('not' r) => (('not' p) '&' ('not' q))) => (('not' (('not' p) '&' ('not' q))) => r) in TAUT A by LUKASI_1:31;
then (('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r) in TAUT A by QC_LANG2:def 3;
then A2: (('not' r) => ('not' q)) => ((('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:13;
((('not' r) => ('not' q)) => ((('not' r) => (('not' p) '&' ('not' q))) => ((p 'or' q) => r))) => (((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) => ((('not' r) => ('not' q)) => ((p 'or' q) => r))) in TAUT A by LUKASI_1:11;
then ((('not' r) => ('not' q)) => (('not' r) => (('not' p) '&' ('not' q)))) => ((('not' r) => ('not' q)) => ((p 'or' q) => r)) in TAUT A by A2, CQC_THE1:46;
then (('not' r) => ('not' p)) => ((('not' r) => ('not' q)) => ((p 'or' q) => r)) in TAUT A by A1, LUKASI_1:3;
then A3: (('not' r) => ('not' q)) => ((('not' r) => ('not' p)) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:15;
(q => r) => (('not' r) => ('not' q)) in TAUT A by LUKASI_1:26;
then (q => r) => ((('not' r) => ('not' p)) => ((p 'or' q) => r)) in TAUT A by A3, LUKASI_1:3;
then A4: (('not' r) => ('not' p)) => ((q => r) => ((p 'or' q) => r)) in TAUT A by LUKASI_1:15;
(p => r) => (('not' r) => ('not' p)) in TAUT A by LUKASI_1:26;
hence (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT A by A4, LUKASI_1:3; :: thesis: verum