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

Theorem syl311anc 1196
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 1132 . 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 1182 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syl312anc  1203  syl321anc  1204  syl313anc  1206  syl331anc  1207  pythagtrip  12887  nmolb2d  18227  nmoleub  18240  cvlcvr1  29529  4atlem12b  29800  dalawlem10  30069  dalawlem13  30072  dalawlem15  30074  osumcllem11N  30155  lhp2atne  30223  lhp2at0ne  30225  cdlemd  30396  ltrneq3  30397  cdleme7d  30435  cdlemeg49le  30700  cdleme  30749  cdlemg1a  30759  ltrniotavalbN  30773  cdlemg44  30922  cdlemk19  31058  cdlemk27-3  31096  cdlemk33N  31098  cdlemk34  31099  cdlemk49  31140  cdlemk53a  31144  cdlemk19u  31159  cdlemk56w  31162  dia2dimlem4  31257  dih1dimatlem0  31518
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