3ccased

Description: Triple disjunction form of ccased . (Contributed by Scott Fenton, 27-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	3ccased.1	$⊢ φ \to ((χ \land η) \to ψ)$
	3ccased.2	$⊢ φ \to ((χ \land ζ) \to ψ)$
	3ccased.3	$⊢ φ \to ((χ \land σ) \to ψ)$
	3ccased.4	$⊢ φ \to ((θ \land η) \to ψ)$
	3ccased.5	$⊢ φ \to ((θ \land ζ) \to ψ)$
	3ccased.6	$⊢ φ \to ((θ \land σ) \to ψ)$
	3ccased.7	$⊢ φ \to ((τ \land η) \to ψ)$
	3ccased.8	$⊢ φ \to ((τ \land ζ) \to ψ)$
	3ccased.9	$⊢ φ \to ((τ \land σ) \to ψ)$
Assertion	3ccased	$⊢ φ \to (((χ \lor θ \lor τ) \land (η \lor ζ \lor σ)) \to ψ)$

Step	Hyp	Ref	Expression
1		3ccased.1	$⊢ φ \to ((χ \land η) \to ψ)$
2		3ccased.2	$⊢ φ \to ((χ \land ζ) \to ψ)$
3		3ccased.3	$⊢ φ \to ((χ \land σ) \to ψ)$
4		3ccased.4	$⊢ φ \to ((θ \land η) \to ψ)$
5		3ccased.5	$⊢ φ \to ((θ \land ζ) \to ψ)$
6		3ccased.6	$⊢ φ \to ((θ \land σ) \to ψ)$
7		3ccased.7	$⊢ φ \to ((τ \land η) \to ψ)$
8		3ccased.8	$⊢ φ \to ((τ \land ζ) \to ψ)$
9		3ccased.9	$⊢ φ \to ((τ \land σ) \to ψ)$
10	1	com12	$⊢ (χ \land η) \to (φ \to ψ)$
11	2	com12	$⊢ (χ \land ζ) \to (φ \to ψ)$
12	3	com12	$⊢ (χ \land σ) \to (φ \to ψ)$
13	10 11 12	3jaodan	$⊢ (χ \land (η \lor ζ \lor σ)) \to (φ \to ψ)$
14	4	com12	$⊢ (θ \land η) \to (φ \to ψ)$
15	5	com12	$⊢ (θ \land ζ) \to (φ \to ψ)$
16	6	com12	$⊢ (θ \land σ) \to (φ \to ψ)$
17	14 15 16	3jaodan	$⊢ (θ \land (η \lor ζ \lor σ)) \to (φ \to ψ)$
18	7	com12	$⊢ (τ \land η) \to (φ \to ψ)$
19	8	com12	$⊢ (τ \land ζ) \to (φ \to ψ)$
20	9	com12	$⊢ (τ \land σ) \to (φ \to ψ)$
21	18 19 20	3jaodan	$⊢ (τ \land (η \lor ζ \lor σ)) \to (φ \to ψ)$
22	13 17 21	3jaoian	$⊢ ((χ \lor θ \lor τ) \land (η \lor ζ \lor σ)) \to (φ \to ψ)$
23	22	com12	$⊢ φ \to (((χ \lor θ \lor τ) \land (η \lor ζ \lor σ)) \to ψ)$

Metamath Proof Explorer