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

Theorem syl123anc 1282
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 535 . 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 1277 1  |-  ( ph  ->  si )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  dvfsumlem2  22975  atbtwnexOLDN  32979  atbtwnex  32980  osumcllem7N  33494  lhpmcvr5N  33559  cdleme22f2  33881  cdlemefs32sn1aw  33948  cdlemg7aN  34159  cdlemg7N  34160  cdlemg8c  34163  cdlemg8  34165  cdlemg11aq  34172  cdlemg12b  34178  cdlemg12e  34181  cdlemg12g  34183  cdlemg13a  34185  cdlemg15a  34189  cdlemg17e  34199  cdlemg18d  34215  cdlemg19a  34217  cdlemg20  34219  cdlemg22  34221  cdlemg28a  34227  cdlemg29  34239  cdlemg44a  34265  cdlemk34  34444  cdlemn11pre  34745  dihord10  34758  dihord2pre  34760  dihmeetlem17N  34858
  Copyright terms: Public domain W3C validator