proveit.logic.booleans.implication.iff_intro
proveit.logic.booleans.implication.true_implies_true