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  13196  nmolb2d  18740  nmoleub  18753  cvlcvr1  29976  4atlem12b  30247  dalawlem10  30516  dalawlem13  30519  dalawlem15  30521  osumcllem11N  30602  lhp2atne  30670  lhp2at0ne  30672  cdlemd  30843  ltrneq3  30844  cdleme7d  30882  cdlemeg49le  31147  cdleme  31196  cdlemg1a  31206  ltrniotavalbN  31220  cdlemg44  31369  cdlemk19  31505  cdlemk27-3  31543  cdlemk33N  31545  cdlemk34  31546  cdlemk49  31587  cdlemk53a  31591  cdlemk19u  31606  cdlemk56w  31609  dia2dimlem4  31704  dih1dimatlem0  31965
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