Theorem pm5.31

Description: Theorem *5.31 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\chi \wedge \left(\phi \to \psi \right)\right)\to \left(\phi \to \psi \right)$$
2		simpl	$$⊢\left(\chi \wedge \left(\phi \to \psi \right)\right)\to \chi$$
3	1 2	jctird	$$⊢\left(\chi \wedge \left(\phi \to \psi \right)\right)\to \left(\phi \to \left(\psi \wedge \chi \right)\right)$$