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