MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl123anc 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  19872  atbtwnexOLDN  29941  atbtwnex  29942  osumcllem7N  30456  lhpmcvr5N  30521  cdleme22f2  30841  cdlemefs32sn1aw  30908  cdlemg7aN  31119  cdlemg7N  31120  cdlemg8c  31123  cdlemg8  31125  cdlemg11aq  31132  cdlemg12b  31138  cdlemg12e  31141  cdlemg12g  31143  cdlemg13a  31145  cdlemg15a  31149  cdlemg17e  31159  cdlemg18d  31175  cdlemg19a  31177  cdlemg20  31179  cdlemg22  31181  cdlemg28a  31187  cdlemg29  31199  cdlemg44a  31225  cdlemk34  31404  cdlemn11pre  31705  dihord10  31718  dihord2pre  31720  dihmeetlem17N  31818
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