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
syl12anc.2
syl12anc.3
syl22anc.4
syl23anc.5
syl33anc.6
syl133anc.7
syl233anc.8
syl332anc.9
Assertion
Ref Expression
syl332anc

Proof of Theorem syl332anc
StepHypRef Expression
1 syl12anc.1 . 2
2 syl12anc.2 . 2
3 syl12anc.3 . 2
4 syl22anc.4 . 2
5 syl23anc.5 . 2
6 syl33anc.6 . 2
7 syl133anc.7 . . 3
8 syl233anc.8 . . 3
97, 8jca 541 . 2
10 syl332anc.9 . 2
111, 2, 3, 4, 5, 6, 9, 10syl331anc 1317 1
 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