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

Theorem syl123anc 1201
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 519 . 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 1196 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  dvfsumlem2  19911  atbtwnexOLDN  30244  atbtwnex  30245  osumcllem7N  30759  lhpmcvr5N  30824  cdleme22f2  31144  cdlemefs32sn1aw  31211  cdlemg7aN  31422  cdlemg7N  31423  cdlemg8c  31426  cdlemg8  31428  cdlemg11aq  31435  cdlemg12b  31441  cdlemg12e  31444  cdlemg12g  31446  cdlemg13a  31448  cdlemg15a  31452  cdlemg17e  31462  cdlemg18d  31478  cdlemg19a  31480  cdlemg20  31482  cdlemg22  31484  cdlemg28a  31490  cdlemg29  31502  cdlemg44a  31528  cdlemk34  31707  cdlemn11pre  32008  dihord10  32021  dihord2pre  32023  dihmeetlem17N  32121
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