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

Theorem syl323anc 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 )
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 520 . 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 1209 1  |-  ( ph  ->  mu )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  4atlem11  30480  dalem52  30595  dath2  30608  dalawlem1  30742  dalaw  30757  cdlemb2  30912  4atexlem7  30946  cdleme7ga  31119  cdleme18a  31162  cdleme18c  31164  cdleme21f  31203  cdleme26f2ALTN  31235  cdleme26f2  31236  cdleme27a  31238  cdlemg17dN  31534  cdlemg18a  31549  cdlemg31d  31571  cdlemg48  31608  cdlemj1  31692  dihord4  32130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator