826.sagews

(A ^ B) ^ ~B -> A

A is TRUE on right of the connective -> for the Statement to be a Tautology it must be TRUE -> TRUE since -> indicates IMPLICATION.

import sage.logic.propcalc as propcalc
One = propcalc.formula("(A & B)");
One.truthtable();

A B value False False False False True False True False False True True True

So we confirmed TRUE & TRUE = TRUE

import sage.logic.propcalc as propcalc
One = propcalc.formula("A & ~B");
One.truthtable();

A B value False False False False True False True False True True True False

Confirmed TRUE & FALSE = TRUE

import sage.logic.propcalc as propcalc
One = propcalc.formula("A -> A");
One.truthtable();

A value False True True True

Confirmed A -> A is always TRUE! TAUTOLOGY!