Theorem pm4.45im

Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)

Conclusion

\( \vdash \varphi \leftrightarrow \varphi \wedge (\psi \rightarrow \varphi) \)

Proof

ax-1

pm4.71i _