let p, q be Element of MC-wff ; :: thesis: ( p '&' q in IPC-Taut iff q '&' p in IPC-Taut )

hereby :: thesis: ( q '&' p in IPC-Taut implies p '&' q in IPC-Taut )

assume A1: p '&' q in IPC-Taut ; :: thesis: q '&' p in IPC-Taut
then A2: q in IPC-Taut by Th34;
p in IPC-Taut by A1, Th34;
hence q '&' p in IPC-Taut by A2, Th34; :: thesis: verum

end;

assume A3: q '&' p in IPC-Taut ; :: thesis: p '&' q in IPC-Taut
then A4: p in IPC-Taut by Th34;
q in IPC-Taut by A3, Th34;
hence p '&' q in IPC-Taut by A4, Th34; :: thesis: verum