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

Theorem syl333anc 1258
Description: A syllogism inference combined with contraction. (Contributed by NM, 10-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 )
sylXanc.9  |-  ( ph  ->  mu )
syl333anc.10  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze )  /\  ( si  /\  rh  /\  mu ) )  ->  la )
Assertion
Ref Expression
syl333anc  |-  ( ph  ->  la )

Proof of Theorem syl333anc
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 )
9 sylXanc.9 . . 3  |-  ( ph  ->  mu )
107, 8, 93jca 1174 . 2  |-  ( ph  ->  ( si  /\  rh  /\  mu ) )
11 syl333anc.10 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze )  /\  ( si  /\  rh  /\  mu ) )  ->  la )
121, 2, 3, 4, 5, 6, 10, 11syl331anc 1251 1  |-  ( ph  ->  la )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ 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:  eengtrkg  24493  ofscom  29888  cgrextend  29889  segconeq  29891  ifscgr  29925  cgrsub  29926  btwnxfr  29937  fscgr  29961  linecgr  29962  btwnconn1lem4  29971  btwnconn1lem5  29972  btwnconn1lem6  29973  btwnconn1lem8  29975  btwnconn1lem11  29978  seglecgr12  29992  colinbtwnle  29999  lshpkrlem6  35256  ps-2c  35668  pmodlem1  35986  pmodlem2  35987  dalawlem4  36014  dalawlem9  36019  4atexlemc  36209  cdleme11l  36410  cdleme15c  36417  cdleme16  36426  cdleme19e  36449  cdleme20l2  36463  cdleme20l  36464  cdleme20m  36465  cdleme20  36466  cdleme21d  36472  cdleme21e  36473  cdleme26ee  36502  cdleme26eALTN  36503  cdleme27a  36509  cdleme28b  36513  cdleme28c  36514  cdleme36m  36603  cdlemg12  36792  cdlemg16ALTN  36800  cdlemg17iqN  36816  cdlemg18c  36822  cdlemg19  36826  cdlemg21  36828  cdlemg28  36846  cdlemk11  36991  cdlemk12  36992  cdlemk16a  36998  cdlemk16  36999  cdlemk18  37010  cdlemk19  37011  cdlemk11u  37013  cdlemk12u  37014  cdlemk21N  37015  cdlemk20  37016  cdlemkoatnle-2N  37017  cdlemk13-2N  37018  cdlemkole-2N  37019  cdlemk14-2N  37020  cdlemk15-2N  37021  cdlemk16-2N  37022  cdlemk17-2N  37023  cdlemk18-2N  37028  cdlemk19-2N  37029  cdlemk7u-2N  37030  cdlemk11u-2N  37031  cdlemk12u-2N  37032  cdlemk22  37035  cdlemk30  37036  cdlemk23-3  37044  cdlemk26b-3  37047  cdlemk26-3  37048  cdlemk27-3  37049  cdlemk11ta  37071  cdlemk47  37091  dia2dimlem1  37207
  Copyright terms: Public domain W3C validator