let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds

( p => q in TAUT A iff ('not' q) => ('not' p) in TAUT A )

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

(p => q) => (('not' q) => ('not' p)) in TAUT A by Th26;

hence ( p => q in TAUT A implies ('not' q) => ('not' p) in TAUT A ) by CQC_THE1:46; :: thesis: ( ('not' q) => ('not' p) in TAUT A implies p => q in TAUT A )

(('not' q) => ('not' p)) => (p => q) in TAUT A by Th24;

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

( p => q in TAUT A iff ('not' q) => ('not' p) in TAUT A )

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

(p => q) => (('not' q) => ('not' p)) in TAUT A by Th26;

hence ( p => q in TAUT A implies ('not' q) => ('not' p) in TAUT A ) by CQC_THE1:46; :: thesis: ( ('not' q) => ('not' p) in TAUT A implies p => q in TAUT A )

(('not' q) => ('not' p)) => (p => q) in TAUT A by Th24;

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