Theorem pm5.31r

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

	Ref	Expression
Assertion	pm5.31r	⊢ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1	⊢ ( 𝜒 → ( 𝜑 → 𝜒 ) )
2		id	⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) )
3	1 2	anim12ii	⊢ ( ( 𝜒 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )