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

Theorem syl231anc 1238
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 1231 1  |-  ( ph  ->  si )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  syl232anc  1245  isosctr  22224  axeuclid  23214  dalawlem3  33522  dalawlem6  33525  cdlemd7  33853  cdleme18c  33942  cdlemi  34469  cdlemk7  34497  cdlemk11  34498  cdlemk7u  34519  cdlemk11u  34520  cdlemk19xlem  34591  cdlemk55u1  34614  cdlemk56  34620
  Copyright terms: Public domain W3C validator