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

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