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

Theorem syl33anc 1233
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 1168 . 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 1220 1  |-  ( ph  ->  si )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  mdetunilem9  18445  mdetuni0  18446  xmetrtri  19949  bl2in  19994  blhalf  19999  blssps  20018  blss  20019  blcld  20099  methaus  20114  metdstri  20446  metdscnlem  20450  metnrmlem3  20456  xlebnum  20556  pmltpclem1  20951  tanord1  22012  basellem1  22437  perfectlem2  22588  bposlem6  22647  dchrisum0flblem2  22777  pntpbnd1a  22853  colinearalglem2  23172  axlowdim  23226  ssbnd  28710  totbndbnd  28711  heiborlem6  28738  2atm  33194  lplncvrlvol2  33282  dalem19  33349  paddasslem9  33495  pclclN  33558  pclfinN  33567  pclfinclN  33617  pexmidlem8N  33644  trlval3  33854  cdleme22b  34008  cdlemefr29bpre0N  34073  cdlemefr29clN  34074  cdlemefr32fvaN  34076  cdlemefr32fva1  34077  cdlemg31b0N  34361  cdlemg31b0a  34362  cdlemh  34484  dihmeetlem16N  34990  dihmeetlem18N  34992  dihmeetlem19N  34993  dihmeetlem20N  34994
  Copyright terms: Public domain W3C validator