Theorem pm5.31r

Variant of pm5.31. (Contributed by Rodolfo Medina, 15-Oct-2010.)

Conclusion
\( \vdash \chi \wedge (\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \chi \wedge \psi \)
Proof
l0
ax-1
id
anim12ii l0 _