let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al st p is valid & p => q is valid holds
q is valid
let p, q be Element of CQC-WFF Al; :: thesis: ( p is valid & p => q is valid implies q is valid )
A1: TAUT Al is being_a_theory by Th11;
assume ( p is valid & p => q is valid ) ; :: thesis: q is valid
then ( p in TAUT Al & p => q in TAUT Al ) ;
then q in TAUT Al by A1;
hence q is valid ; :: thesis: verum