Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3ccased Unicode version

Theorem 3ccased 24073
Description: Triple disjunction form of ccased 913. (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
StepHypRef Expression
1 3ccased.1 . . . . 5  |-  ( ph  ->  ( ( ch  /\  et )  ->  ps )
)
21com12 27 . . . 4  |-  ( ( ch  /\  et )  ->  ( ph  ->  ps ) )
3 3ccased.2 . . . . 5  |-  ( ph  ->  ( ( ch  /\  ze )  ->  ps )
)
43com12 27 . . . 4  |-  ( ( ch  /\  ze )  ->  ( ph  ->  ps ) )
5 3ccased.3 . . . . 5  |-  ( ph  ->  ( ( ch  /\  si )  ->  ps )
)
65com12 27 . . . 4  |-  ( ( ch  /\  si )  ->  ( ph  ->  ps ) )
72, 4, 63jaodan 1248 . . 3  |-  ( ( ch  /\  ( et  \/  ze  \/  si ) )  ->  ( ph  ->  ps ) )
8 3ccased.4 . . . . 5  |-  ( ph  ->  ( ( th  /\  et )  ->  ps )
)
98com12 27 . . . 4  |-  ( ( th  /\  et )  ->  ( ph  ->  ps ) )
10 3ccased.5 . . . . 5  |-  ( ph  ->  ( ( th  /\  ze )  ->  ps )
)
1110com12 27 . . . 4  |-  ( ( th  /\  ze )  ->  ( ph  ->  ps ) )
12 3ccased.6 . . . . 5  |-  ( ph  ->  ( ( th  /\  si )  ->  ps )
)
1312com12 27 . . . 4  |-  ( ( th  /\  si )  ->  ( ph  ->  ps ) )
149, 11, 133jaodan 1248 . . 3  |-  ( ( th  /\  ( et  \/  ze  \/  si ) )  ->  ( ph  ->  ps ) )
15 3ccased.7 . . . . 5  |-  ( ph  ->  ( ( ta  /\  et )  ->  ps )
)
1615com12 27 . . . 4  |-  ( ( ta  /\  et )  ->  ( ph  ->  ps ) )
17 3ccased.8 . . . . 5  |-  ( ph  ->  ( ( ta  /\  ze )  ->  ps )
)
1817com12 27 . . . 4  |-  ( ( ta  /\  ze )  ->  ( ph  ->  ps ) )
19 3ccased.9 . . . . 5  |-  ( ph  ->  ( ( ta  /\  si )  ->  ps )
)
2019com12 27 . . . 4  |-  ( ( ta  /\  si )  ->  ( ph  ->  ps ) )
2116, 18, 203jaodan 1248 . . 3  |-  ( ( ta  /\  ( et  \/  ze  \/  si ) )  ->  ( ph  ->  ps ) )
227, 14, 213jaoian 1247 . 2  |-  ( ( ( ch  \/  th  \/  ta )  /\  ( et  \/  ze  \/  si ) )  ->  ( ph  ->  ps ) )
2322com12 27 1  |-  ( ph  ->  ( ( ( ch  \/  th  \/  ta )  /\  ( et  \/  ze  \/  si ) )  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    \/ w3o 933
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936
  Copyright terms: Public domain W3C validator