let A be QC-alphabet ; :: thesis: for p, q, s being Element of CQC-WFF A holds (s => (q => p)) => (q => (s => p)) in TAUT A

let p, q, s be Element of CQC-WFF A; :: thesis: (s => (q => p)) => (q => (s => p)) in TAUT A

( q => ((q => p) => p) in TAUT A & (q => ((q => p) => p)) => ((s => (q => p)) => (q => (s => p))) in TAUT A ) by Lm2, Th7;

hence (s => (q => p)) => (q => (s => p)) in TAUT A by CQC_THE1:46; :: thesis: verum

let p, q, s be Element of CQC-WFF A; :: thesis: (s => (q => p)) => (q => (s => p)) in TAUT A

( q => ((q => p) => p) in TAUT A & (q => ((q => p) => p)) => ((s => (q => p)) => (q => (s => p))) in TAUT A ) by Lm2, Th7;

hence (s => (q => p)) => (q => (s => p)) in TAUT A by CQC_THE1:46; :: thesis: verum