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  19374  atbtwnexOLDN  29636  atbtwnex  29637  osumcllem7N  30151  lhpmcvr5N  30216  cdleme22f2  30536  cdlemefs32sn1aw  30603  cdlemg7aN  30814  cdlemg7N  30815  cdlemg8c  30818  cdlemg8  30820  cdlemg11aq  30827  cdlemg12b  30833  cdlemg12e  30836  cdlemg12g  30838  cdlemg13a  30840  cdlemg15a  30844  cdlemg17e  30854  cdlemg18d  30870  cdlemg19a  30872  cdlemg20  30874  cdlemg22  30876  cdlemg28a  30882  cdlemg29  30894  cdlemg44a  30920  cdlemk34  31099  cdlemn11pre  31400  dihord10  31413  dihord2pre  31415  dihmeetlem17N  31513
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