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