iscnrm3lem4

Step	Hyp	Ref	Expression
1		iscnrm3lem4.1	$⊢ η \to (ψ \to ζ)$
2		iscnrm3lem4.2	$⊢ (φ \land χ \land θ) \to η$
3		iscnrm3lem4.3	$⊢ (φ \land χ \land θ) \to (ζ \to τ)$
4		iscnrm3lem3	$⊢ ((φ \land ψ) \land (χ \land θ)) \leftrightarrow ((φ \land χ \land θ) \land ψ)$
5	2 1	syl	$⊢ (φ \land χ \land θ) \to (ψ \to ζ)$
6	5 3	syld	$⊢ (φ \land χ \land θ) \to (ψ \to τ)$
7	6	imp	$⊢ ((φ \land χ \land θ) \land ψ) \to τ$
8	4 7	sylbi	$⊢ ((φ \land ψ) \land (χ \land θ)) \to τ$
9	8	exp43	$⊢ φ \to (ψ \to (χ \to (θ \to τ)))$

Metamath Proof Explorer