824.sagews

[(A->B)^A] ->B

B is TRUE so we want to verify the other side of the connective is also true.

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

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

We see TRUE -> TRUE = TRUE

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

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

We see TRUE & TRUE = TRUE

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

B value False True True True

TRUE -> TRUE = TAUTOLOGY