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

Theorem syl123anc 1199
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 )
sylXanc.6  |-  ( ph  ->  ze )
syl123anc.7  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et  /\  ze ) )  ->  si )
Assertion
Ref Expression
syl123anc  |-  ( ph  ->  si )

Proof of Theorem syl123anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
42, 3jca 518 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 sylXanc.5 . 2  |-  ( ph  ->  et )
7 sylXanc.6 . 2  |-  ( ph  ->  ze )
8 syl123anc.7 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ( ta  /\  et  /\  ze ) )  ->  si )
91, 4, 5, 6, 7, 8syl113anc 1194 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  dvfsumlem2  19390  atbtwnexOLDN  30258  atbtwnex  30259  osumcllem7N  30773  lhpmcvr5N  30838  cdleme22f2  31158  cdlemefs32sn1aw  31225  cdlemg7aN  31436  cdlemg7N  31437  cdlemg8c  31440  cdlemg8  31442  cdlemg11aq  31449  cdlemg12b  31455  cdlemg12e  31458  cdlemg12g  31460  cdlemg13a  31462  cdlemg15a  31466  cdlemg17e  31476  cdlemg18d  31492  cdlemg19a  31494  cdlemg20  31496  cdlemg22  31498  cdlemg28a  31504  cdlemg29  31516  cdlemg44a  31542  cdlemk34  31721  cdlemn11pre  32022  dihord10  32035  dihord2pre  32037  dihmeetlem17N  32135
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