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

Theorem syl233anc 1211
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
sylXanc.6  |-  ( ph  ->  ze )
sylXanc.7  |-  ( ph  ->  si )
sylXanc.8  |-  ( ph  ->  rh )
syl233anc.9  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta  /\  et )  /\  ( ze  /\  si  /\  rh ) )  ->  mu )
Assertion
Ref Expression
syl233anc  |-  ( ph  ->  mu )

Proof of Theorem syl233anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 518 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylXanc.3 . 2  |-  ( ph  ->  th )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 sylXanc.5 . 2  |-  ( ph  ->  et )
7 sylXanc.6 . 2  |-  ( ph  ->  ze )
8 sylXanc.7 . 2  |-  ( ph  ->  si )
9 sylXanc.8 . 2  |-  ( ph  ->  rh )
10 syl233anc.9 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta  /\  et )  /\  ( ze  /\  si  /\  rh ) )  ->  mu )
113, 4, 5, 6, 7, 8, 9, 10syl133anc 1205 1  |-  ( ph  ->  mu )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  2llnjN  29829  cdleme16b  30541  cdleme18d  30557  cdleme19d  30568  cdleme20bN  30572  cdleme20l1  30582  cdleme22cN  30604  cdleme22eALTN  30607  cdleme22f  30608  cdlemg33c0  30964  cdlemk5  31098  cdlemk5u  31123  cdlemky  31188  cdlemkyyN  31224
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-an 360  df-3an 936
  Copyright terms: Public domain W3C validator