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  17935  bl2in  17973  blhalf  17976  blss  17988  blcld  18067  methaus  18082  metdstri  18371  metdscnlem  18375  metnrmlem3  18381  xlebnum  18479  pmltpclem1  18824  tanord1  19915  basellem1  20334  perfectlem2  20485  bposlem6  20544  dchrisum0flblem2  20674  pntpbnd1a  20750  colinearalglem2  24607  axlowdim  24661  lvsovso  25729  ssbnd  26615  totbndbnd  26616  heiborlem6  26643  2atm  30338  lplncvrlvol2  30426  dalem19  30493  paddasslem9  30639  pclclN  30702  pclfinN  30711  pclfinclN  30761  pexmidlem8N  30788  trlval3  30998  cdleme22b  31152  cdlemefr29bpre0N  31217  cdlemefr29clN  31218  cdlemefr32fvaN  31220  cdlemefr32fva1  31221  cdlemg31b0N  31505  cdlemg31b0a  31506  cdlemh  31628  dihmeetlem16N  32134  dihmeetlem18N  32136  dihmeetlem19N  32137  dihmeetlem20N  32138
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