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

Theorem syl33anc 1245
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 1177 . 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 1232 1  |-  ( ph  ->  si )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  initoeu2lem2  15510  mdetunilem9  19306  mdetuni0  19307  xmetrtri  21042  bl2in  21087  blhalf  21092  blssps  21111  blss  21112  blcld  21192  methaus  21207  metdstri  21539  metdscnlem  21543  metnrmlem3  21549  xlebnum  21649  pmltpclem1  22044  tanord1  23108  basellem1  23627  perfectlem2  23778  bposlem6  23837  dchrisum0flblem2  23967  pntpbnd1a  24043  colinearalglem2  24508  axlowdim  24562  ssbnd  31547  totbndbnd  31548  heiborlem6  31575  2atm  32525  lplncvrlvol2  32613  dalem19  32680  paddasslem9  32826  pclclN  32889  pclfinN  32898  pclfinclN  32948  pexmidlem8N  32975  trlval3  33186  cdleme22b  33341  cdlemefr29bpre0N  33406  cdlemefr29clN  33407  cdlemefr32fvaN  33409  cdlemefr32fva1  33410  cdlemg31b0N  33694  cdlemg31b0a  33695  cdlemh  33817  dihmeetlem16N  34323  dihmeetlem18N  34325  dihmeetlem19N  34326  dihmeetlem20N  34327
  Copyright terms: Public domain W3C validator