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;
( (p => r) => ((q => r) => ((p 'or' q) => r)) in TAUT & ((p => r) => ((q => r) => ((p 'or' q) => r))) => (((p => r) '&' (q => r)) => ((p 'or' q) => r)) in TAUT ) by Th32, Th35;
hence ((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT by CQC_THE1:46; :: thesis: verum