let p, q, s be Element of MC-wff ; :: thesis: ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut
A1: (q '&' s) => (s '&' q) in IPC-Taut by Th46;
((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut by Th45;
hence ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut by A1, Th26; :: thesis: verum