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

Theorem syl231anc 1248
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 532 . 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 1241 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:  syl232anc  1255  isosctr  22911  axeuclid  23970  dalawlem3  34687  dalawlem6  34690  cdlemd7  35018  cdleme18c  35107  cdlemi  35634  cdlemk7  35662  cdlemk11  35663  cdlemk7u  35684  cdlemk11u  35685  cdlemk19xlem  35756  cdlemk55u1  35779  cdlemk56  35785
  Copyright terms: Public domain W3C validator