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 p '&' q in IPC-Taut ; :: thesis: q '&' p in IPC-Taut
then ( p in IPC-Taut & q in IPC-Taut ) by Th34;
hence q '&' p in IPC-Taut by Th34; :: thesis: verum

end;

assume q '&' p in IPC-Taut ; :: thesis: p '&' q in IPC-Taut
then ( q in IPC-Taut & p in IPC-Taut ) by Th34;
hence p '&' q in IPC-Taut by Th34; :: thesis: verum