ccased

Step	Hyp	Ref	Expression
1		ccased.1	$⊢ φ \to ((ψ \land χ) \to η)$
2		ccased.2	$⊢ φ \to ((θ \land χ) \to η)$
3		ccased.3	$⊢ φ \to ((ψ \land τ) \to η)$
4		ccased.4	$⊢ φ \to ((θ \land τ) \to η)$
5	1	com12	$⊢ (ψ \land χ) \to (φ \to η)$
6	2	com12	$⊢ (θ \land χ) \to (φ \to η)$
7	3	com12	$⊢ (ψ \land τ) \to (φ \to η)$
8	4	com12	$⊢ (θ \land τ) \to (φ \to η)$
9	5 6 7 8	ccase	$⊢ ((ψ \lor θ) \land (χ \lor τ)) \to (φ \to η)$
10	9	com12	$⊢ φ \to (((ψ \lor θ) \land (χ \lor τ)) \to η)$

Metamath Proof Explorer