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

Theorem syl323anc 1256
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 530 . 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 1250 1  |-  ( ph  ->  mu )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  4atlem11  35730  dalem52  35845  dath2  35858  dalawlem1  35992  dalaw  36007  cdlemb2  36162  4atexlem7  36196  cdleme7ga  36370  cdleme18a  36413  cdleme18c  36415  cdleme21f  36455  cdleme26f2ALTN  36487  cdleme26f2  36488  cdleme27a  36490  cdlemg17dN  36786  cdlemg18a  36801  cdlemg31d  36823  cdlemg48  36860  cdlemj1  36944  dihord4  37382
  Copyright terms: Public domain W3C validator