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

Theorem syl332anc 1213
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 )
syl332anc.9  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze )  /\  ( si  /\  rh ) )  ->  mu )
Assertion
Ref Expression
syl332anc  |-  ( ph  ->  mu )

Proof of Theorem syl332anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . 2  |-  ( ph  ->  ta )
5 sylXanc.5 . 2  |-  ( ph  ->  et )
6 sylXanc.6 . 2  |-  ( ph  ->  ze )
7 sylXanc.7 . . 3  |-  ( ph  ->  si )
8 sylXanc.8 . . 3  |-  ( ph  ->  rh )
97, 8jca 518 . 2  |-  ( ph  ->  ( si  /\  rh ) )
10 syl332anc.9 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze )  /\  ( si  /\  rh ) )  ->  mu )
111, 2, 3, 4, 5, 6, 9, 10syl331anc 1207 1  |-  ( ph  ->  mu )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  lnjatN  30591  lncmp  30594  cdlema1N  30602  4atexlemex6  30885  cdlemd4  31012  cdleme18c  31104  cdleme18d  31106  cdleme19b  31115  cdleme21ct  31140  cdleme21d  31141  cdleme21e  31142  cdleme21k  31149  cdleme22g  31159  cdleme24  31163  cdleme27a  31178  cdleme27N  31180  cdleme28a  31181  cdleme40n  31279  cdlemg16zz  31471  cdlemg37  31500  cdlemk21-2N  31702  cdlemk20-2N  31703  cdlemk28-3  31719  cdlemk19xlem  31753
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