Theorem anim12d1

Description: Variant of anim12d where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010)

	Ref	Expression
Hypotheses	anim12d1.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	anim12d1.2	⊢ ( 𝜃 → 𝜏 )
Assertion	anim12d1	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		anim12d1.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		anim12d1.2	⊢ ( 𝜃 → 𝜏 )
3	2	a1i	⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) )
4	1 3	anim12d	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜏 ) ) )