let p, q be Element of MC-wff ; :: thesis: ( p is valid_IPC & p => q is valid_IPC implies q is valid_IPC )
A1: IPC-Taut is IPC_theory ;
assume ( p is valid_IPC & p => q is valid_IPC ) ; :: thesis: q is valid_IPC
then ( p in IPC-Taut & p => q in IPC-Taut ) ;
hence q is valid_IPC by A1; :: thesis: verum