let s, q, p be Element of CQC-WFF ; :: thesis: ( s => (q => p) in TAUT & q in TAUT implies s => p in TAUT )
assume s => (q => p) in TAUT ; :: thesis: ( not q in TAUT or s => p in TAUT )
then q => (s => p) in TAUT by Th15;
hence ( not q in TAUT or s => p in TAUT ) by CQC_THE1:82; :: thesis: verum