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

Theorem syl33anc 1238
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 1171 . 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 1225 1  |-  ( ph  ->  si )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 185  df-an 371  df-3an 970
This theorem is referenced by:  mdetunilem9  18882  mdetuni0  18883  xmetrtri  20586  bl2in  20631  blhalf  20636  blssps  20655  blss  20656  blcld  20736  methaus  20751  metdstri  21083  metdscnlem  21087  metnrmlem3  21093  xlebnum  21193  pmltpclem1  21588  tanord1  22650  basellem1  23075  perfectlem2  23226  bposlem6  23285  dchrisum0flblem2  23415  pntpbnd1a  23491  colinearalglem2  23879  axlowdim  23933  ssbnd  29874  totbndbnd  29875  heiborlem6  29902  2atm  34198  lplncvrlvol2  34286  dalem19  34353  paddasslem9  34499  pclclN  34562  pclfinN  34571  pclfinclN  34621  pexmidlem8N  34648  trlval3  34858  cdleme22b  35012  cdlemefr29bpre0N  35077  cdlemefr29clN  35078  cdlemefr32fvaN  35080  cdlemefr32fva1  35081  cdlemg31b0N  35365  cdlemg31b0a  35366  cdlemh  35488  dihmeetlem16N  35994  dihmeetlem18N  35996  dihmeetlem19N  35997  dihmeetlem20N  35998
  Copyright terms: Public domain W3C validator