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

Theorem syl333anc 1324
Description: A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1  |-  ( ph  ->  ps )
syl12anc.2  |-  ( ph  ->  ch )
syl12anc.3  |-  ( ph  ->  th )
syl22anc.4  |-  ( ph  ->  ta )
syl23anc.5  |-  ( ph  ->  et )
syl33anc.6  |-  ( ph  ->  ze )
syl133anc.7  |-  ( ph  ->  si )
syl233anc.8  |-  ( ph  ->  rh )
syl333anc.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 syl12anc.1 . 2  |-  ( ph  ->  ps )
2 syl12anc.2 . 2  |-  ( ph  ->  ch )
3 syl12anc.3 . 2  |-  ( ph  ->  th )
4 syl22anc.4 . 2  |-  ( ph  ->  ta )
5 syl23anc.5 . 2  |-  ( ph  ->  et )
6 syl33anc.6 . 2  |-  ( ph  ->  ze )
7 syl133anc.7 . . 3  |-  ( ph  ->  si )
8 syl233anc.8 . . 3  |-  ( ph  ->  rh )
9 syl333anc.9 . . 3  |-  ( ph  ->  mu )
107, 8, 93jca 1210 . 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 1317 1  |-  ( ph  ->  la )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  eengtrkg  25094  ofscom  30845  cgrextend  30846  segconeq  30848  ifscgr  30882  cgrsub  30883  btwnxfr  30894  fscgr  30918  linecgr  30919  btwnconn1lem4  30928  btwnconn1lem5  30929  btwnconn1lem6  30930  btwnconn1lem8  30932  btwnconn1lem11  30935  seglecgr12  30949  colinbtwnle  30956  lshpkrlem6  32752  ps-2c  33164  pmodlem1  33482  pmodlem2  33483  dalawlem4  33510  dalawlem9  33515  4atexlemc  33705  cdleme11l  33906  cdleme15c  33913  cdleme16  33922  cdleme19e  33945  cdleme20l2  33959  cdleme20l  33960  cdleme20m  33961  cdleme20  33962  cdleme21d  33968  cdleme21e  33969  cdleme26ee  33998  cdleme26eALTN  33999  cdleme27a  34005  cdleme28b  34009  cdleme28c  34010  cdleme36m  34099  cdlemg12  34288  cdlemg16ALTN  34296  cdlemg17iqN  34312  cdlemg18c  34318  cdlemg19  34322  cdlemg21  34324  cdlemg28  34342  cdlemk11  34487  cdlemk12  34488  cdlemk16a  34494  cdlemk16  34495  cdlemk18  34506  cdlemk19  34507  cdlemk11u  34509  cdlemk12u  34510  cdlemk21N  34511  cdlemk20  34512  cdlemkoatnle-2N  34513  cdlemk13-2N  34514  cdlemkole-2N  34515  cdlemk14-2N  34516  cdlemk15-2N  34517  cdlemk16-2N  34518  cdlemk17-2N  34519  cdlemk18-2N  34524  cdlemk19-2N  34525  cdlemk7u-2N  34526  cdlemk11u-2N  34527  cdlemk12u-2N  34528  cdlemk22  34531  cdlemk30  34532  cdlemk23-3  34540  cdlemk26b-3  34543  cdlemk26-3  34544  cdlemk27-3  34545  cdlemk11ta  34567  cdlemk47  34587  dia2dimlem1  34703
  Copyright terms: Public domain W3C validator