let p, r, q be Element of CQC-WFF ; :: thesis: ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT
set P = p => r;
set Q = q => r;
set R = (p 'or' q) => r;
A1: (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT by Th35;
((p => r) => ((q => r) => ((p 'or' q) => r))) => (((p => r) '&' (q => r)) => ((p 'or' q) => r)) in TAUT by Th32;
hence ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT by A1, CQC_THE1:82; :: thesis: verum