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	|- ( ph -> ( ( ch /\ et ) -> ps ) )
	3ccased.2	|- ( ph -> ( ( ch /\ ze ) -> ps ) )
	3ccased.3	|- ( ph -> ( ( ch /\ si ) -> ps ) )
	3ccased.4	|- ( ph -> ( ( th /\ et ) -> ps ) )
	3ccased.5	|- ( ph -> ( ( th /\ ze ) -> ps ) )
	3ccased.6	|- ( ph -> ( ( th /\ si ) -> ps ) )
	3ccased.7	|- ( ph -> ( ( ta /\ et ) -> ps ) )
	3ccased.8	|- ( ph -> ( ( ta /\ ze ) -> ps ) )
	3ccased.9	|- ( ph -> ( ( ta /\ si ) -> ps ) )
Assertion	3ccased	|- ( ph -> ( ( ( ch \/ th \/ ta ) /\ ( et \/ ze \/ si ) ) -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		3ccased.1	|- ( ph -> ( ( ch /\ et ) -> ps ) )
2		3ccased.2	|- ( ph -> ( ( ch /\ ze ) -> ps ) )
3		3ccased.3	|- ( ph -> ( ( ch /\ si ) -> ps ) )
4		3ccased.4	|- ( ph -> ( ( th /\ et ) -> ps ) )
5		3ccased.5	|- ( ph -> ( ( th /\ ze ) -> ps ) )
6		3ccased.6	|- ( ph -> ( ( th /\ si ) -> ps ) )
7		3ccased.7	|- ( ph -> ( ( ta /\ et ) -> ps ) )
8		3ccased.8	|- ( ph -> ( ( ta /\ ze ) -> ps ) )
9		3ccased.9	|- ( ph -> ( ( ta /\ si ) -> ps ) )
10	1	com12	|- ( ( ch /\ et ) -> ( ph -> ps ) )
11	2	com12	|- ( ( ch /\ ze ) -> ( ph -> ps ) )
12	3	com12	|- ( ( ch /\ si ) -> ( ph -> ps ) )
13	10 11 12	3jaodan	|- ( ( ch /\ ( et \/ ze \/ si ) ) -> ( ph -> ps ) )
14	4	com12	|- ( ( th /\ et ) -> ( ph -> ps ) )
15	5	com12	|- ( ( th /\ ze ) -> ( ph -> ps ) )
16	6	com12	|- ( ( th /\ si ) -> ( ph -> ps ) )
17	14 15 16	3jaodan	|- ( ( th /\ ( et \/ ze \/ si ) ) -> ( ph -> ps ) )
18	7	com12	|- ( ( ta /\ et ) -> ( ph -> ps ) )
19	8	com12	|- ( ( ta /\ ze ) -> ( ph -> ps ) )
20	9	com12	|- ( ( ta /\ si ) -> ( ph -> ps ) )
21	18 19 20	3jaodan	|- ( ( ta /\ ( et \/ ze \/ si ) ) -> ( ph -> ps ) )
22	13 17 21	3jaoian	|- ( ( ( ch \/ th \/ ta ) /\ ( et \/ ze \/ si ) ) -> ( ph -> ps ) )
23	22	com12	|- ( ph -> ( ( ( ch \/ th \/ ta ) /\ ( et \/ ze \/ si ) ) -> ps ) )