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

Theorem ccased 914
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 29 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  et ) )
3 ccased.2 . . . 4  |-  ( ph  ->  ( ( th  /\  ch )  ->  et ) )
43com12 29 . . 3  |-  ( ( th  /\  ch )  ->  ( ph  ->  et ) )
5 ccased.3 . . . 4  |-  ( ph  ->  ( ( ps  /\  ta )  ->  et ) )
65com12 29 . . 3  |-  ( ( ps  /\  ta )  ->  ( ph  ->  et ) )
7 ccased.4 . . . 4  |-  ( ph  ->  ( ( th  /\  ta )  ->  et ) )
87com12 29 . . 3  |-  ( ( th  /\  ta )  ->  ( ph  ->  et ) )
92, 4, 6, 8ccase 913 . 2  |-  ( ( ( ps  \/  th )  /\  ( ch  \/  ta ) )  ->  ( ph  ->  et ) )
109com12 29 1  |-  ( ph  ->  ( ( ( ps  \/  th )  /\  ( ch  \/  ta ) )  ->  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    /\ wa 359
This theorem is referenced by:  fpwwe2lem13  8481  mulge0  9509  zmulcl  10288  gcdabs  12996  pospo  14393  mulgass  14883  indistopon  17028  lgsdir2lem5  21072  outsideofeq  25976  smprngopr  26560  monotoddzzfi  26903  acongtr  26941  cdlemg33  31205
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator