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

Theorem syl311anc 1243
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 )
syl311anc.6  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta  /\  et )  ->  ze )
Assertion
Ref Expression
syl311anc  |-  ( ph  ->  ze )

Proof of Theorem syl311anc
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 syl311anc.6 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta  /\  et )  ->  ze )
84, 5, 6, 7syl3anc 1229 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ 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 371  df-3an 976
This theorem is referenced by:  syl312anc  1250  syl321anc  1251  syl313anc  1253  syl331anc  1254  pythagtrip  14340  nmolb2d  21203  nmoleub  21216  clwwisshclwwlem  24784  cvlcvr1  34939  4atlem12b  35210  dalawlem10  35479  dalawlem13  35482  dalawlem15  35484  osumcllem11N  35565  lhp2atne  35633  lhp2at0ne  35635  cdlemd  35807  ltrneq3  35808  cdleme7d  35846  cdlemeg49le  36112  cdleme  36161  cdlemg1a  36171  ltrniotavalbN  36185  cdlemg44  36334  cdlemk19  36470  cdlemk27-3  36508  cdlemk33N  36510  cdlemk34  36511  cdlemk49  36552  cdlemk53a  36556  cdlemk19u  36571  cdlemk56w  36574  dia2dimlem4  36669  dih1dimatlem0  36930
  Copyright terms: Public domain W3C validator