let p, r, q be Element of CQC-WFF ; :: thesis: ( p => r in TAUT & q => r in TAUT implies (p 'or' q) => r in TAUT )
assume ( p => r in TAUT & q => r in TAUT ) ; :: thesis: (p 'or' q) => r in TAUT
then A1: (p => r) '&' (q => r) in TAUT by Lm4;
((p => r) '&' (q => r)) => ((p 'or' q) => r) in TAUT by Th36;
hence (p 'or' q) => r in TAUT by A1, CQC_THE1:82; :: thesis: verum