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

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

assume A1: p '&' q in IPC-Taut ; :: thesis: ( p in IPC-Taut & q in IPC-Taut )
( (p '&' q) => p in IPC-Taut & (p '&' q) => q in IPC-Taut ) by Def14;
hence ( p in IPC-Taut & q in IPC-Taut ) by A1, Def14; :: thesis: verum

end;

assume A2: ( p in IPC-Taut & q in IPC-Taut ) ; :: thesis: p '&' q in IPC-Taut
p => (q => (p '&' q)) in IPC-Taut by Def14;
then q => (p '&' q) in IPC-Taut by A2, Def14;
hence p '&' q in IPC-Taut by A2, Def14; :: thesis: verum