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

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

assume A1: p '&' q in HP_TAUT ; :: thesis: q '&' p in HP_TAUT
then A2: q in HP_TAUT by Th31;
p in HP_TAUT by A1, Th31;
hence q '&' p in HP_TAUT by A2, Th31; :: thesis: verum

end;

assume A3: q '&' p in HP_TAUT ; :: thesis: p '&' q in HP_TAUT
then A4: p in HP_TAUT by Th31;
q in HP_TAUT by A3, Th31;
hence p '&' q in HP_TAUT by A4, Th31; :: thesis: verum