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