Theorem 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	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜂 ) → 𝜓 ) )
	3ccased.2	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜁 ) → 𝜓 ) )
	3ccased.3	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜎 ) → 𝜓 ) )
	3ccased.4	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜂 ) → 𝜓 ) )
	3ccased.5	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜁 ) → 𝜓 ) )
	3ccased.6	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜎 ) → 𝜓 ) )
	3ccased.7	⊢ ( 𝜑 → ( ( 𝜏 ∧ 𝜂 ) → 𝜓 ) )
	3ccased.8	⊢ ( 𝜑 → ( ( 𝜏 ∧ 𝜁 ) → 𝜓 ) )
	3ccased.9	⊢ ( 𝜑 → ( ( 𝜏 ∧ 𝜎 ) → 𝜓 ) )
Assertion	3ccased	⊢ ( 𝜑 → ( ( ( 𝜒 ∨ 𝜃 ∨ 𝜏 ) ∧ ( 𝜂 ∨ 𝜁 ∨ 𝜎 ) ) → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		3ccased.1	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜂 ) → 𝜓 ) )
2		3ccased.2	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜁 ) → 𝜓 ) )
3		3ccased.3	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜎 ) → 𝜓 ) )
4		3ccased.4	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜂 ) → 𝜓 ) )
5		3ccased.5	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜁 ) → 𝜓 ) )
6		3ccased.6	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜎 ) → 𝜓 ) )
7		3ccased.7	⊢ ( 𝜑 → ( ( 𝜏 ∧ 𝜂 ) → 𝜓 ) )
8		3ccased.8	⊢ ( 𝜑 → ( ( 𝜏 ∧ 𝜁 ) → 𝜓 ) )
9		3ccased.9	⊢ ( 𝜑 → ( ( 𝜏 ∧ 𝜎 ) → 𝜓 ) )
10	1	com12	⊢ ( ( 𝜒 ∧ 𝜂 ) → ( 𝜑 → 𝜓 ) )
11	2	com12	⊢ ( ( 𝜒 ∧ 𝜁 ) → ( 𝜑 → 𝜓 ) )
12	3	com12	⊢ ( ( 𝜒 ∧ 𝜎 ) → ( 𝜑 → 𝜓 ) )
13	10 11 12	3jaodan	⊢ ( ( 𝜒 ∧ ( 𝜂 ∨ 𝜁 ∨ 𝜎 ) ) → ( 𝜑 → 𝜓 ) )
14	4	com12	⊢ ( ( 𝜃 ∧ 𝜂 ) → ( 𝜑 → 𝜓 ) )
15	5	com12	⊢ ( ( 𝜃 ∧ 𝜁 ) → ( 𝜑 → 𝜓 ) )
16	6	com12	⊢ ( ( 𝜃 ∧ 𝜎 ) → ( 𝜑 → 𝜓 ) )
17	14 15 16	3jaodan	⊢ ( ( 𝜃 ∧ ( 𝜂 ∨ 𝜁 ∨ 𝜎 ) ) → ( 𝜑 → 𝜓 ) )
18	7	com12	⊢ ( ( 𝜏 ∧ 𝜂 ) → ( 𝜑 → 𝜓 ) )
19	8	com12	⊢ ( ( 𝜏 ∧ 𝜁 ) → ( 𝜑 → 𝜓 ) )
20	9	com12	⊢ ( ( 𝜏 ∧ 𝜎 ) → ( 𝜑 → 𝜓 ) )
21	18 19 20	3jaodan	⊢ ( ( 𝜏 ∧ ( 𝜂 ∨ 𝜁 ∨ 𝜎 ) ) → ( 𝜑 → 𝜓 ) )
22	13 17 21	3jaoian	⊢ ( ( ( 𝜒 ∨ 𝜃 ∨ 𝜏 ) ∧ ( 𝜂 ∨ 𝜁 ∨ 𝜎 ) ) → ( 𝜑 → 𝜓 ) )
23	22	com12	⊢ ( 𝜑 → ( ( ( 𝜒 ∨ 𝜃 ∨ 𝜏 ) ∧ ( 𝜂 ∨ 𝜁 ∨ 𝜎 ) ) → 𝜓 ) )