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

Theorem syl311anc 1237
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 1171 . 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 1223 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 970
This theorem is referenced by:  syl312anc  1244  syl321anc  1245  syl313anc  1247  syl331anc  1248  pythagtrip  14206  nmolb2d  20953  nmoleub  20966  clwwisshclwwlem  24468  cvlcvr1  34011  4atlem12b  34282  dalawlem10  34551  dalawlem13  34554  dalawlem15  34556  osumcllem11N  34637  lhp2atne  34705  lhp2at0ne  34707  cdlemd  34878  ltrneq3  34879  cdleme7d  34917  cdlemeg49le  35182  cdleme  35231  cdlemg1a  35241  ltrniotavalbN  35255  cdlemg44  35404  cdlemk19  35540  cdlemk27-3  35578  cdlemk33N  35580  cdlemk34  35581  cdlemk49  35622  cdlemk53a  35626  cdlemk19u  35641  cdlemk56w  35644  dia2dimlem4  35739  dih1dimatlem0  36000
  Copyright terms: Public domain W3C validator