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