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

Theorem syl233anc 1255
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 )
sylXanc.7  |-  ( ph  ->  si )
sylXanc.8  |-  ( ph  ->  rh )
syl233anc.9  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta  /\  et )  /\  ( ze  /\  si  /\  rh ) )  ->  mu )
Assertion
Ref Expression
syl233anc  |-  ( ph  ->  mu )

Proof of Theorem syl233anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 530 . 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 sylXanc.7 . 2  |-  ( ph  ->  si )
9 sylXanc.8 . 2  |-  ( ph  ->  rh )
10 syl233anc.9 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta  /\  et )  /\  ( ze  /\  si  /\  rh ) )  ->  mu )
113, 4, 5, 6, 7, 8, 9, 10syl133anc 1249 1  |-  ( ph  ->  mu )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  br8d  27681  2llnjN  35707  cdleme16b  36420  cdleme18d  36436  cdleme19d  36448  cdleme20bN  36452  cdleme20l1  36462  cdleme22cN  36484  cdleme22eALTN  36487  cdleme22f  36488  cdlemg33c0  36844  cdlemk5  36978  cdlemk5u  37003  cdlemky  37068  cdlemkyyN  37104
  Copyright terms: Public domain W3C validator