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

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

Proof of Theorem syl332anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . 2  |-  ( ph  ->  ta )
5 sylXanc.5 . 2  |-  ( ph  ->  et )
6 sylXanc.6 . 2  |-  ( ph  ->  ze )
7 sylXanc.7 . . 3  |-  ( ph  ->  si )
8 sylXanc.8 . . 3  |-  ( ph  ->  rh )
97, 8jca 519 . 2  |-  ( ph  ->  ( si  /\  rh ) )
10 syl332anc.9 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze )  /\  ( si  /\  rh ) )  ->  mu )
111, 2, 3, 4, 5, 6, 9, 10syl331anc 1209 1  |-  ( ph  ->  mu )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  lnjatN  30514  lncmp  30517  cdlema1N  30525  4atexlemex6  30808  cdlemd4  30935  cdleme18c  31027  cdleme18d  31029  cdleme19b  31038  cdleme21ct  31063  cdleme21d  31064  cdleme21e  31065  cdleme21k  31072  cdleme22g  31082  cdleme24  31086  cdleme27a  31101  cdleme27N  31103  cdleme28a  31104  cdleme40n  31202  cdlemg16zz  31394  cdlemg37  31423  cdlemk21-2N  31625  cdlemk20-2N  31626  cdlemk28-3  31642  cdlemk19xlem  31676
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator