proveit.logic.equality.rhs_via_equality
proveit.logic.booleans.implication.iff_implies_right
proveit.logic.booleans.conjunction.right_from_and