let p, q be Element of MC-wff ; :: thesis: ( q in IPC-Taut implies p => q in IPC-Taut )
q => (p => q) in IPC-Taut by Def14;
hence ( q in IPC-Taut implies p => q in IPC-Taut ) by Def14; :: thesis: verum