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

Theorem syl332anc 1215
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 519 . 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 1209 1  |-  ( ph  ->  mu )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  lnjatN  29896  lncmp  29899  cdlema1N  29907  4atexlemex6  30190  cdlemd4  30317  cdleme18c  30409  cdleme18d  30411  cdleme19b  30420  cdleme21ct  30445  cdleme21d  30446  cdleme21e  30447  cdleme21k  30454  cdleme22g  30464  cdleme24  30468  cdleme27a  30483  cdleme27N  30485  cdleme28a  30486  cdleme40n  30584  cdlemg16zz  30776  cdlemg37  30805  cdlemk21-2N  31007  cdlemk20-2N  31008  cdlemk28-3  31024  cdlemk19xlem  31058
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-an 361  df-3an 938
  Copyright terms: Public domain W3C validator