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

Theorem syl333anc 1301
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 1189 . 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 1294 1  |-  ( ph  ->  la )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 986
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 189  df-an 373  df-3an 988
This theorem is referenced by:  eengtrkg  25027  ofscom  30786  cgrextend  30787  segconeq  30789  ifscgr  30823  cgrsub  30824  btwnxfr  30835  fscgr  30859  linecgr  30860  btwnconn1lem4  30869  btwnconn1lem5  30870  btwnconn1lem6  30871  btwnconn1lem8  30873  btwnconn1lem11  30876  seglecgr12  30890  colinbtwnle  30897  lshpkrlem6  32693  ps-2c  33105  pmodlem1  33423  pmodlem2  33424  dalawlem4  33451  dalawlem9  33456  4atexlemc  33646  cdleme11l  33847  cdleme15c  33854  cdleme16  33863  cdleme19e  33886  cdleme20l2  33900  cdleme20l  33901  cdleme20m  33902  cdleme20  33903  cdleme21d  33909  cdleme21e  33910  cdleme26ee  33939  cdleme26eALTN  33940  cdleme27a  33946  cdleme28b  33950  cdleme28c  33951  cdleme36m  34040  cdlemg12  34229  cdlemg16ALTN  34237  cdlemg17iqN  34253  cdlemg18c  34259  cdlemg19  34263  cdlemg21  34265  cdlemg28  34283  cdlemk11  34428  cdlemk12  34429  cdlemk16a  34435  cdlemk16  34436  cdlemk18  34447  cdlemk19  34448  cdlemk11u  34450  cdlemk12u  34451  cdlemk21N  34452  cdlemk20  34453  cdlemkoatnle-2N  34454  cdlemk13-2N  34455  cdlemkole-2N  34456  cdlemk14-2N  34457  cdlemk15-2N  34458  cdlemk16-2N  34459  cdlemk17-2N  34460  cdlemk18-2N  34465  cdlemk19-2N  34466  cdlemk7u-2N  34467  cdlemk11u-2N  34468  cdlemk12u-2N  34469  cdlemk22  34472  cdlemk30  34473  cdlemk23-3  34481  cdlemk26b-3  34484  cdlemk26-3  34485  cdlemk27-3  34486  cdlemk11ta  34508  cdlemk47  34528  dia2dimlem1  34644
  Copyright terms: Public domain W3C validator