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

Theorem syl311anc 1198
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 1134 . 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 1184 1  |-  ( ph  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syl312anc  1205  syl321anc  1206  syl313anc  1208  syl331anc  1209  pythagtrip  13167  nmolb2d  18709  nmoleub  18722  cvlcvr1  29826  4atlem12b  30097  dalawlem10  30366  dalawlem13  30369  dalawlem15  30371  osumcllem11N  30452  lhp2atne  30520  lhp2at0ne  30522  cdlemd  30693  ltrneq3  30694  cdleme7d  30732  cdlemeg49le  30997  cdleme  31046  cdlemg1a  31056  ltrniotavalbN  31070  cdlemg44  31219  cdlemk19  31355  cdlemk27-3  31393  cdlemk33N  31395  cdlemk34  31396  cdlemk49  31437  cdlemk53a  31441  cdlemk19u  31456  cdlemk56w  31459  dia2dimlem4  31554  dih1dimatlem0  31815
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