3anim123d

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

	Ref	Expression
Hypotheses	3anim123d.1	$⊢ φ \to (ψ \to χ)$
	3anim123d.2	$⊢ φ \to (θ \to τ)$
	3anim123d.3	$⊢ φ \to (η \to ζ)$
Assertion	3anim123d	$⊢ φ \to ((ψ \land θ \land η) \to (χ \land τ \land ζ))$

Step	Hyp	Ref	Expression
1		3anim123d.1	$⊢ φ \to (ψ \to χ)$
2		3anim123d.2	$⊢ φ \to (θ \to τ)$
3		3anim123d.3	$⊢ φ \to (η \to ζ)$
4	1 2	anim12d	$⊢ φ \to ((ψ \land θ) \to (χ \land τ))$
5	4 3	anim12d	$⊢ φ \to (((ψ \land θ) \land η) \to ((χ \land τ) \land ζ))$
6		df-3an	$⊢ (ψ \land θ \land η) \leftrightarrow ((ψ \land θ) \land η)$
7		df-3an	$⊢ (χ \land τ \land ζ) \leftrightarrow ((χ \land τ) \land ζ)$
8	5 6 7	3imtr4g	$⊢ φ \to ((ψ \land θ \land η) \to (χ \land τ \land ζ))$

Metamath Proof Explorer