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

Theorem syl333anc 1217
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 1135 . 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 1210 1  |-  ( ph  ->  la )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  ofscom  25943  cgrextend  25944  segconeq  25946  ifscgr  25980  cgrsub  25981  btwnxfr  25992  fscgr  26016  linecgr  26017  btwnconn1lem4  26026  btwnconn1lem5  26027  btwnconn1lem6  26028  btwnconn1lem8  26030  btwnconn1lem11  26033  seglecgr12  26047  colinbtwnle  26054  lshpkrlem6  29915  ps-2c  30327  pmodlem1  30645  pmodlem2  30646  dalawlem4  30673  dalawlem9  30678  4atexlemc  30868  cdleme11l  31068  cdleme15c  31075  cdleme16  31084  cdleme19e  31106  cdleme20l2  31120  cdleme20l  31121  cdleme20m  31122  cdleme20  31123  cdleme21d  31129  cdleme21e  31130  cdleme26ee  31159  cdleme26eALTN  31160  cdleme27a  31166  cdleme28b  31170  cdleme28c  31171  cdleme36m  31260  cdlemg12  31449  cdlemg16ALTN  31457  cdlemg17iqN  31473  cdlemg18c  31479  cdlemg19  31483  cdlemg21  31485  cdlemg28  31503  cdlemk11  31648  cdlemk12  31649  cdlemk16a  31655  cdlemk16  31656  cdlemk18  31667  cdlemk19  31668  cdlemk11u  31670  cdlemk12u  31671  cdlemk21N  31672  cdlemk20  31673  cdlemkoatnle-2N  31674  cdlemk13-2N  31675  cdlemkole-2N  31676  cdlemk14-2N  31677  cdlemk15-2N  31678  cdlemk16-2N  31679  cdlemk17-2N  31680  cdlemk18-2N  31685  cdlemk19-2N  31686  cdlemk7u-2N  31687  cdlemk11u-2N  31688  cdlemk12u-2N  31689  cdlemk22  31692  cdlemk30  31693  cdlemk23-3  31701  cdlemk26b-3  31704  cdlemk26-3  31705  cdlemk27-3  31706  cdlemk11ta  31728  cdlemk47  31748  dia2dimlem1  31864
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator