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  8264  mulge0  9291  zmulcl  10066  gcdabs  12712  pospo  14107  mulgass  14597  indistopon  16738  lgsdir2lem5  20566  outsideofeq  24753  smprngopr  26677  monotoddzzfi  27027  acongtr  27065  cdlemg33  30900
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