let p, q be Element of HP-WFF ; :: thesis: ( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )

hereby :: thesis: ( p in HP_TAUT & q in HP_TAUT implies p '&' q in HP_TAUT )

A1: (p '&' q) => q in HP_TAUT by Def10;
assume A2: p '&' q in HP_TAUT ; :: thesis: ( p in HP_TAUT & q in HP_TAUT )
(p '&' q) => p in HP_TAUT by Def10;
hence ( p in HP_TAUT & q in HP_TAUT ) by A2, A1, Def10; :: thesis: verum

end;

assume that
A3: p in HP_TAUT and
A4: q in HP_TAUT ; :: thesis: p '&' q in HP_TAUT
p => (q => (p '&' q)) in HP_TAUT by Def10;
then q => (p '&' q) in HP_TAUT by A3, Def10;
hence p '&' q in HP_TAUT by A4, Def10; :: thesis: verum