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

Theorem syl33anc 1197
Description: Syllogism combined with contraction. (Contributed by NM, 11-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 )
syl33anc.7  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze ) )  ->  si )
Assertion
Ref Expression
syl33anc  |-  ( ph  ->  si )

Proof of Theorem syl33anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1132 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 sylXanc.5 . 2  |-  ( ph  ->  et )
7 sylXanc.6 . 2  |-  ( ph  ->  ze )
8 syl33anc.7 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze ) )  ->  si )
94, 5, 6, 7, 8syl13anc 1184 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  xmetrtri  17919  bl2in  17957  blhalf  17960  blss  17972  blcld  18051  methaus  18066  metdstri  18355  metdscnlem  18359  metnrmlem3  18365  xlebnum  18463  pmltpclem1  18808  tanord1  19899  basellem1  20318  perfectlem2  20469  bposlem6  20528  dchrisum0flblem2  20658  pntpbnd1a  20734  colinearalglem2  24535  axlowdim  24589  lvsovso  25626  ssbnd  26512  totbndbnd  26513  heiborlem6  26540  2atm  29716  lplncvrlvol2  29804  dalem19  29871  paddasslem9  30017  pclclN  30080  pclfinN  30089  pclfinclN  30139  pexmidlem8N  30166  trlval3  30376  cdleme22b  30530  cdlemefr29bpre0N  30595  cdlemefr29clN  30596  cdlemefr32fvaN  30598  cdlemefr32fva1  30599  cdlemg31b0N  30883  cdlemg31b0a  30884  cdlemh  31006  dihmeetlem16N  31512  dihmeetlem18N  31514  dihmeetlem19N  31515  dihmeetlem20N  31516
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator