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

Theorem syl231anc 1205
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 520 . 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 1198 1  |-  ( ph  ->  si )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  syl232anc  1212  isosctr  20666  axeuclid  25903  dalawlem3  30671  dalawlem6  30674  cdlemd7  31002  cdleme18c  31091  cdlemi  31618  cdlemk7  31646  cdlemk11  31647  cdlemk7u  31668  cdlemk11u  31669  cdlemk19xlem  31740  cdlemk55u1  31763  cdlemk56  31769
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator