theorem Th34: :: INTPRO_1:34

for p, q being Element of MC-wff holds
( p '&' q in IPC-Taut iff ( p in IPC-Taut & q in IPC-Taut ) )