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

Theorem syl33anc 1199
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 1134 . 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 1186 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  xmetrtri  18385  bl2in  18430  blhalf  18435  blssps  18454  blss  18455  blcld  18535  methaus  18550  metdstri  18881  metdscnlem  18885  metnrmlem3  18891  xlebnum  18990  pmltpclem1  19345  tanord1  20439  basellem1  20863  perfectlem2  21014  bposlem6  21073  dchrisum0flblem2  21203  pntpbnd1a  21279  colinearalglem2  25846  axlowdim  25900  ssbnd  26497  totbndbnd  26498  heiborlem6  26525  2atm  30324  lplncvrlvol2  30412  dalem19  30479  paddasslem9  30625  pclclN  30688  pclfinN  30697  pclfinclN  30747  pexmidlem8N  30774  trlval3  30984  cdleme22b  31138  cdlemefr29bpre0N  31203  cdlemefr29clN  31204  cdlemefr32fvaN  31206  cdlemefr32fva1  31207  cdlemg31b0N  31491  cdlemg31b0a  31492  cdlemh  31614  dihmeetlem16N  32120  dihmeetlem18N  32122  dihmeetlem19N  32123  dihmeetlem20N  32124
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator