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  12984  nmolb2d  18329  nmoleub  18342  cvlcvr1  29598  4atlem12b  29869  dalawlem10  30138  dalawlem13  30141  dalawlem15  30143  osumcllem11N  30224  lhp2atne  30292  lhp2at0ne  30294  cdlemd  30465  ltrneq3  30466  cdleme7d  30504  cdlemeg49le  30769  cdleme  30818  cdlemg1a  30828  ltrniotavalbN  30842  cdlemg44  30991  cdlemk19  31127  cdlemk27-3  31165  cdlemk33N  31167  cdlemk34  31168  cdlemk49  31209  cdlemk53a  31213  cdlemk19u  31228  cdlemk56w  31231  dia2dimlem4  31326  dih1dimatlem0  31587
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