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

Theorem syl123anc 1243
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 530 . 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 1238 1  |-  ( ph  ->  si )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  dvfsumlem2  22513  atbtwnexOLDN  35584  atbtwnex  35585  osumcllem7N  36099  lhpmcvr5N  36164  cdleme22f2  36486  cdlemefs32sn1aw  36553  cdlemg7aN  36764  cdlemg7N  36765  cdlemg8c  36768  cdlemg8  36770  cdlemg11aq  36777  cdlemg12b  36783  cdlemg12e  36786  cdlemg12g  36788  cdlemg13a  36790  cdlemg15a  36794  cdlemg17e  36804  cdlemg18d  36820  cdlemg19a  36822  cdlemg20  36824  cdlemg22  36826  cdlemg28a  36832  cdlemg29  36844  cdlemg44a  36870  cdlemk34  37049  cdlemn11pre  37350  dihord10  37363  dihord2pre  37365  dihmeetlem17N  37463
  Copyright terms: Public domain W3C validator