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