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 )

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

end;

assume that
A3: p in IPC-Taut and
A4: 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 A3, Def14;
hence p '&' q in IPC-Taut by A4, Def14; :: thesis: verum