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  19780  atbtwnexOLDN  29563  atbtwnex  29564  osumcllem7N  30078  lhpmcvr5N  30143  cdleme22f2  30463  cdlemefs32sn1aw  30530  cdlemg7aN  30741  cdlemg7N  30742  cdlemg8c  30745  cdlemg8  30747  cdlemg11aq  30754  cdlemg12b  30760  cdlemg12e  30763  cdlemg12g  30765  cdlemg13a  30767  cdlemg15a  30771  cdlemg17e  30781  cdlemg18d  30797  cdlemg19a  30799  cdlemg20  30801  cdlemg22  30803  cdlemg28a  30809  cdlemg29  30821  cdlemg44a  30847  cdlemk34  31026  cdlemn11pre  31327  dihord10  31340  dihord2pre  31342  dihmeetlem17N  31440
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