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

Theorem syl333anc 1296
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 1185 . 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 1289 1  |-  ( ph  ->  la )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  eengtrkg  25001  ofscom  30766  cgrextend  30767  segconeq  30769  ifscgr  30803  cgrsub  30804  btwnxfr  30815  fscgr  30839  linecgr  30840  btwnconn1lem4  30849  btwnconn1lem5  30850  btwnconn1lem6  30851  btwnconn1lem8  30853  btwnconn1lem11  30856  seglecgr12  30870  colinbtwnle  30877  lshpkrlem6  32599  ps-2c  33011  pmodlem1  33329  pmodlem2  33330  dalawlem4  33357  dalawlem9  33362  4atexlemc  33552  cdleme11l  33753  cdleme15c  33760  cdleme16  33769  cdleme19e  33792  cdleme20l2  33806  cdleme20l  33807  cdleme20m  33808  cdleme20  33809  cdleme21d  33815  cdleme21e  33816  cdleme26ee  33845  cdleme26eALTN  33846  cdleme27a  33852  cdleme28b  33856  cdleme28c  33857  cdleme36m  33946  cdlemg12  34135  cdlemg16ALTN  34143  cdlemg17iqN  34159  cdlemg18c  34165  cdlemg19  34169  cdlemg21  34171  cdlemg28  34189  cdlemk11  34334  cdlemk12  34335  cdlemk16a  34341  cdlemk16  34342  cdlemk18  34353  cdlemk19  34354  cdlemk11u  34356  cdlemk12u  34357  cdlemk21N  34358  cdlemk20  34359  cdlemkoatnle-2N  34360  cdlemk13-2N  34361  cdlemkole-2N  34362  cdlemk14-2N  34363  cdlemk15-2N  34364  cdlemk16-2N  34365  cdlemk17-2N  34366  cdlemk18-2N  34371  cdlemk19-2N  34372  cdlemk7u-2N  34373  cdlemk11u-2N  34374  cdlemk12u-2N  34375  cdlemk22  34378  cdlemk30  34379  cdlemk23-3  34387  cdlemk26b-3  34390  cdlemk26-3  34391  cdlemk27-3  34392  cdlemk11ta  34414  cdlemk47  34434  dia2dimlem1  34550
  Copyright terms: Public domain W3C validator