let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds
( (('not' ('not' p)) => q) => (p => q) in TAUT A & (p => q) => (('not' ('not' p)) => q) in TAUT A )
let p, q be Element of CQC-WFF A; :: thesis: ( (('not' ('not' p)) => q) => (p => q) in TAUT A & (p => q) => (('not' ('not' p)) => q) in TAUT A )
p => ('not' ('not' p)) in TAUT A by Th27;
hence (('not' ('not' p)) => q) => (p => q) in TAUT A by Th2; :: thesis: (p => q) => (('not' ('not' p)) => q) in TAUT A
('not' ('not' p)) => p in TAUT A by Th25;
hence (p => q) => (('not' ('not' p)) => q) in TAUT A by Th2; :: thesis: verum