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  29969  lncmp  29972  cdlema1N  29980  4atexlemex6  30263  cdlemd4  30390  cdleme18c  30482  cdleme18d  30484  cdleme19b  30493  cdleme21ct  30518  cdleme21d  30519  cdleme21e  30520  cdleme21k  30527  cdleme22g  30537  cdleme24  30541  cdleme27a  30556  cdleme27N  30558  cdleme28a  30559  cdleme40n  30657  cdlemg16zz  30849  cdlemg37  30878  cdlemk21-2N  31080  cdlemk20-2N  31081  cdlemk28-3  31097  cdlemk19xlem  31131
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