This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm5.31r

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

		Ref	Expression
	Assertion	pm5.31r	$⊢ (χ \land (φ \to ψ)) \to (φ \to (χ \land ψ))$

Step	Hyp	Ref	Expression
1		ax-1	$⊢ χ \to (φ \to χ)$
2		id	$⊢ (φ \to ψ) \to (φ \to ψ)$
3	1 2	anim12ii	$⊢ (χ \land (φ \to ψ)) \to (φ \to (χ \land ψ))$