Theorem pm5.31r

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

	Ref	Expression
Assertion	pm5.31r	$$⊢\left(\chi \wedge \left(\phi \to \psi \right)\right)\to \left(\phi \to \left(\chi \wedge \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$$⊢\chi \to \left(\phi \to \chi \right)$$
2		id	$$⊢\left(\phi \to \psi \right)\to \left(\phi \to \psi \right)$$
3	1 2	anim12ii	$$⊢\left(\chi \wedge \left(\phi \to \psi \right)\right)\to \left(\phi \to \left(\chi \wedge \psi \right)\right)$$