import proveit
from proveit import A, B
from proveit.logic.booleans.conjunction import true_and_true
theory = proveit.Theory() # the theorem's theory
%proving and_if_both
AeqT = A.evaluation(assumptions=[A])
BeqT = B.evaluation(assumptions=[B])
true_and_true
AandT = AeqT.sub_left_side_into(true_and_true.inner_expr().operands[0],
auto_simplify=False)
AandB = BeqT.sub_left_side_into(AandT, assumptions=[A, B],
auto_simplify=False)
# To do this manually, execute AandB.generalize((A, B), conditions=[A, B]).
# But this can be figured out via automation.
%qed