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

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

(p => q) => ((q => p) => ((p => q) '&' (q => p))) in TAUT A by Th28;

hence (p => q) => ((q => p) => (p <=> q)) in TAUT A by QC_LANG2:def 4; :: thesis: verum

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

(p => q) => ((q => p) => ((p => q) '&' (q => p))) in TAUT A by Th28;

hence (p => q) => ((q => p) => (p <=> q)) in TAUT A by QC_LANG2:def 4; :: thesis: verum