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

Theorem syl231anc 1202
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 )
syl231anc.7  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta  /\  et )  /\  ze )  ->  si )
Assertion
Ref Expression
syl231anc  |-  ( ph  ->  si )

Proof of Theorem syl231anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 518 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylXanc.3 . 2  |-  ( ph  ->  th )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 sylXanc.5 . 2  |-  ( ph  ->  et )
7 sylXanc.6 . 2  |-  ( ph  ->  ze )
8 syl231anc.7 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta  /\  et )  /\  ze )  ->  si )
93, 4, 5, 6, 7, 8syl131anc 1195 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl232anc  1209  isosctr  20121  axeuclid  24591  dalawlem3  30062  dalawlem6  30065  cdlemd7  30393  cdleme18c  30482  cdlemi  31009  cdlemk7  31037  cdlemk11  31038  cdlemk7u  31059  cdlemk11u  31060  cdlemk19xlem  31131  cdlemk55u1  31154  cdlemk56  31160
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator