Theorem 3ccased 36453

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

Hypotheses

Ref	Expression
3ccased.1	⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓))
3ccased.2	⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓))
3ccased.3	⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓))
3ccased.4	⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓))
3ccased.5	⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓))
3ccased.6	⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓))
3ccased.7	⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓))
3ccased.8	⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓))
3ccased.9	⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓))

Assertion

Ref	Expression
3ccased	⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓))

Proof of Theorem 3ccased

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105

This theorem is used by: (None)