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