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

Theorem syl311anc 1240
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 1174 . 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 1226 1  |-  ( ph  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  syl312anc  1247  syl321anc  1248  syl313anc  1250  syl331anc  1251  pythagtrip  14360  nmolb2d  21310  nmoleub  21323  clwwisshclwwlem  24927  cvlcvr1  35477  4atlem12b  35748  dalawlem10  36017  dalawlem13  36020  dalawlem15  36022  osumcllem11N  36103  lhp2atne  36171  lhp2at0ne  36173  cdlemd  36345  ltrneq3  36346  cdleme7d  36384  cdlemeg49le  36650  cdleme  36699  cdlemg1a  36709  ltrniotavalbN  36723  cdlemg44  36872  cdlemk19  37008  cdlemk27-3  37046  cdlemk33N  37048  cdlemk34  37049  cdlemk49  37090  cdlemk53a  37094  cdlemk19u  37109  cdlemk56w  37112  dia2dimlem4  37207  dih1dimatlem0  37468
  Copyright terms: Public domain W3C validator