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