Theorem iba

Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.)

Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \psi \wedge \varphi) \)
Proof
l0
pm3.21
simpl
impbid1 l0 _