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  20137  axeuclid  24663  dalawlem3  30684  dalawlem6  30687  cdlemd7  31015  cdleme18c  31104  cdlemi  31631  cdlemk7  31659  cdlemk11  31660  cdlemk7u  31681  cdlemk11u  31682  cdlemk19xlem  31753  cdlemk55u1  31776  cdlemk56  31782
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