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

Theorem syl123anc 1245
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 532 . 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 1240 1  |-  ( ph  ->  si )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  dvfsumlem2  22163  atbtwnexOLDN  34243  atbtwnex  34244  osumcllem7N  34758  lhpmcvr5N  34823  cdleme22f2  35143  cdlemefs32sn1aw  35210  cdlemg7aN  35421  cdlemg7N  35422  cdlemg8c  35425  cdlemg8  35427  cdlemg11aq  35434  cdlemg12b  35440  cdlemg12e  35443  cdlemg12g  35445  cdlemg13a  35447  cdlemg15a  35451  cdlemg17e  35461  cdlemg18d  35477  cdlemg19a  35479  cdlemg20  35481  cdlemg22  35483  cdlemg28a  35489  cdlemg29  35501  cdlemg44a  35527  cdlemk34  35706  cdlemn11pre  36007  dihord10  36020  dihord2pre  36022  dihmeetlem17N  36120
  Copyright terms: Public domain W3C validator