let p, q, s be Element of MC-wff ; :: thesis: (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut
set P = s 'or' p;
set Q = s 'or' q;
A1: s => (s 'or' q) in IPC-Taut by Def14;
A2: (p => q) => (p => (s 'or' q)) in IPC-Taut by Th59;
(s => (s 'or' q)) => ((p => (s 'or' q)) => ((s 'or' p) => (s 'or' q))) in IPC-Taut by Def14;
then (p => (s 'or' q)) => ((s 'or' p) => (s 'or' q)) in IPC-Taut by A1, Def14;
hence (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut by A2, Th26; :: thesis: verum