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

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