Theorem 3ccased 31600

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

Hypotheses

Ref	Expression
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

Ref	Expression
3ccased	|- ( ph -> ( ( ( ch \/ th \/ ta ) /\ ( et \/ ze \/ si ) ) -> ps ) )

Proof of Theorem 3ccased

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

Syntax hints:   -> wi 4   /\ wa 384   \/ w3o 1036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039

This theorem is referenced by: (None)