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

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

Proof of Theorem syl323anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
5 sylXanc.5 . . 3  |-  ( ph  ->  et )
64, 5jca 518 . 2  |-  ( ph  ->  ( ta  /\  et ) )
7 sylXanc.6 . 2  |-  ( ph  ->  ze )
8 sylXanc.7 . 2  |-  ( ph  ->  si )
9 sylXanc.8 . 2  |-  ( ph  ->  rh )
10 syl323anc.9 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et )  /\  ( ze  /\  si  /\  rh ) )  ->  mu )
111, 2, 3, 6, 7, 8, 9, 10syl313anc 1206 1  |-  ( ph  ->  mu )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  4atlem11  29798  dalem52  29913  dath2  29926  dalawlem1  30060  dalaw  30075  cdlemb2  30230  4atexlem7  30264  cdleme7ga  30437  cdleme18a  30480  cdleme18c  30482  cdleme21f  30521  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme27a  30556  cdlemg17dN  30852  cdlemg18a  30867  cdlemg31d  30889  cdlemg48  30926  cdlemj1  31010  dihord4  31448
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