Theorem 3anim123d

Description: Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005)

	Ref	Expression
Hypotheses	3anim123d.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	3anim123d.2	⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) )
	3anim123d.3	⊢ ( 𝜑 → ( 𝜂 → 𝜁 ) )
Assertion	3anim123d	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜃 ∧ 𝜂 ) → ( 𝜒 ∧ 𝜏 ∧ 𝜁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3anim123d.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		3anim123d.2	⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) )
3		3anim123d.3	⊢ ( 𝜑 → ( 𝜂 → 𝜁 ) )
4	1 2	anim12d	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜃 ) → ( 𝜒 ∧ 𝜏 ) ) )
5	4 3	anim12d	⊢ ( 𝜑 → ( ( ( 𝜓 ∧ 𝜃 ) ∧ 𝜂 ) → ( ( 𝜒 ∧ 𝜏 ) ∧ 𝜁 ) ) )
6		df-3an	⊢ ( ( 𝜓 ∧ 𝜃 ∧ 𝜂 ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∧ 𝜂 ) )
7		df-3an	⊢ ( ( 𝜒 ∧ 𝜏 ∧ 𝜁 ) ↔ ( ( 𝜒 ∧ 𝜏 ) ∧ 𝜁 ) )
8	5 6 7	3imtr4g	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜃 ∧ 𝜂 ) → ( 𝜒 ∧ 𝜏 ∧ 𝜁 ) ) )