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

Theorem ccased 915
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 30 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  et ) )
3 ccased.2 . . . 4  |-  ( ph  ->  ( ( th  /\  ch )  ->  et ) )
43com12 30 . . 3  |-  ( ( th  /\  ch )  ->  ( ph  ->  et ) )
5 ccased.3 . . . 4  |-  ( ph  ->  ( ( ps  /\  ta )  ->  et ) )
65com12 30 . . 3  |-  ( ( ps  /\  ta )  ->  ( ph  ->  et ) )
7 ccased.4 . . . 4  |-  ( ph  ->  ( ( th  /\  ta )  ->  et ) )
87com12 30 . . 3  |-  ( ( th  /\  ta )  ->  ( ph  ->  et ) )
92, 4, 6, 8ccase 914 . 2  |-  ( ( ( ps  \/  th )  /\  ( ch  \/  ta ) )  ->  ( ph  ->  et ) )
109com12 30 1  |-  ( ph  ->  ( ( ( ps  \/  th )  /\  ( ch  \/  ta ) )  ->  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359    /\ wa 360
This theorem is referenced by:  fpwwe2lem13  8522  mulge0  9550  zmulcl  10329  gcdabs  13038  pospo  14435  mulgass  14925  indistopon  17070  lgsdir2lem5  21116  outsideofeq  26069  smprngopr  26675  monotoddzzfi  27018  acongtr  27056  cdlemg33  31581
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 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator