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

Theorem syl332anc 1323
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1  |-  ( ph  ->  ps )
syl12anc.2  |-  ( ph  ->  ch )
syl12anc.3  |-  ( ph  ->  th )
syl22anc.4  |-  ( ph  ->  ta )
syl23anc.5  |-  ( ph  ->  et )
syl33anc.6  |-  ( ph  ->  ze )
syl133anc.7  |-  ( ph  ->  si )
syl233anc.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 syl12anc.1 . 2  |-  ( ph  ->  ps )
2 syl12anc.2 . 2  |-  ( ph  ->  ch )
3 syl12anc.3 . 2  |-  ( ph  ->  th )
4 syl22anc.4 . 2  |-  ( ph  ->  ta )
5 syl23anc.5 . 2  |-  ( ph  ->  et )
6 syl33anc.6 . 2  |-  ( ph  ->  ze )
7 syl133anc.7 . . 3  |-  ( ph  ->  si )
8 syl233anc.8 . . 3  |-  ( ph  ->  rh )
97, 8jca 541 . 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 1317 1  |-  ( ph  ->  mu )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  mdetunilem5  19718  mdetuni0  19723  lnjatN  33416  lncmp  33419  cdlema1N  33427  4atexlemex6  33710  cdlemd4  33838  cdleme18c  33930  cdleme18d  33932  cdleme19b  33942  cdleme21ct  33967  cdleme21d  33968  cdleme21e  33969  cdleme21k  33976  cdleme22g  33986  cdleme24  33990  cdleme27a  34005  cdleme27N  34007  cdleme28a  34008  cdleme40n  34106  cdlemg16zz  34298  cdlemg37  34327  cdlemk21-2N  34529  cdlemk20-2N  34530  cdlemk28-3  34546  cdlemk19xlem  34580
  Copyright terms: Public domain W3C validator