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

Theorem syl323anc 1214
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 519 . 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 1208 1  |-  ( ph  ->  mu )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  4atlem11  30095  dalem52  30210  dath2  30223  dalawlem1  30357  dalaw  30372  cdlemb2  30527  4atexlem7  30561  cdleme7ga  30734  cdleme18a  30777  cdleme18c  30779  cdleme21f  30818  cdleme26f2ALTN  30850  cdleme26f2  30851  cdleme27a  30853  cdlemg17dN  31149  cdlemg18a  31164  cdlemg31d  31186  cdlemg48  31223  cdlemj1  31307  dihord4  31745
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