let p, q, r, s be Element of CQC-WFF ; :: thesis: ( p => (q => r) in TAUT & p => (r => s) in TAUT implies p => (q => s) in TAUT )
assume that
A1: p => (q => r) in TAUT and
A2: p => (r => s) in TAUT ; :: thesis: p => (q => s) in TAUT
p => ((q => r) => ((r => s) => (q => s))) in TAUT by Th1, Th13;
then p => ((r => s) => (q => s)) in TAUT by A1, Th20;
hence p => (q => s) in TAUT by A2, Th20; :: thesis: verum