MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ccased Unicode version

Theorem ccased 913
Description: Deduction for combining cases. (Contributed by NM, 9-May-2004.)
Hypotheses
Ref Expression
ccased.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  et ) )
ccased.2  |-  ( ph  ->  ( ( th  /\  ch )  ->  et ) )
ccased.3  |-  ( ph  ->  ( ( ps  /\  ta )  ->  et ) )
ccased.4  |-  ( ph  ->  ( ( th  /\  ta )  ->  et ) )
Assertion
Ref Expression
ccased  |-  ( ph  ->  ( ( ( ps  \/  th )  /\  ( ch  \/  ta ) )  ->  et ) )

Proof of Theorem ccased
StepHypRef Expression
1 ccased.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch )  ->  et ) )
21com12 27 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  et ) )
3 ccased.2 . . . 4  |-  ( ph  ->  ( ( th  /\  ch )  ->  et ) )
43com12 27 . . 3  |-  ( ( th  /\  ch )  ->  ( ph  ->  et ) )
5 ccased.3 . . . 4  |-  ( ph  ->  ( ( ps  /\  ta )  ->  et ) )
65com12 27 . . 3  |-  ( ( ps  /\  ta )  ->  ( ph  ->  et ) )
7 ccased.4 . . . 4  |-  ( ph  ->  ( ( th  /\  ta )  ->  et ) )
87com12 27 . . 3  |-  ( ( th  /\  ta )  ->  ( ph  ->  et ) )
92, 4, 6, 8ccase 912 . 2  |-  ( ( ( ps  \/  th )  /\  ( ch  \/  ta ) )  ->  ( ph  ->  et ) )
109com12 27 1  |-  ( ph  ->  ( ( ( ps  \/  th )  /\  ( ch  \/  ta ) )  ->  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    /\ wa 358
This theorem is referenced by:  fpwwe2lem13  8351  mulge0  9378  zmulcl  10155  gcdabs  12803  pospo  14200  mulgass  14690  indistopon  16838  lgsdir2lem5  20672  outsideofeq  25312  smprngopr  26000  monotoddzzfi  26350  acongtr  26388  cdlemg33  30952
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
  Copyright terms: Public domain W3C validator