let p, q be Element of CQC-WFF ; :: thesis: ( p is valid & p => q is valid implies q is valid )
assume A1: ( p is valid & p => q is valid ) ; :: thesis: q is valid
A2: ( p in TAUT & p => q in TAUT ) by A1, Lm13;
A3: q in TAUT by A2, Def1, Th76;
thus q is valid by A3, Lm13; :: thesis: verum