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

Theorem syl332anc 1259
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
sylXanc.5
sylXanc.6
sylXanc.7
sylXanc.8
syl332anc.9
Assertion
Ref Expression
syl332anc

Proof of Theorem syl332anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . 2
3 sylXanc.3 . 2
4 sylXanc.4 . 2
5 sylXanc.5 . 2
6 sylXanc.6 . 2
7 sylXanc.7 . . 3
8 sylXanc.8 . . 3
97, 8jca 532 . 2
10 syl332anc.9 . 2
111, 2, 3, 4, 5, 6, 9, 10syl331anc 1253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  mdetunilem5  19118  mdetuni0  19123  lnjatN  35504  lncmp  35507  cdlema1N  35515  4atexlemex6  35798  cdlemd4  35926  cdleme18c  36018  cdleme18d  36020  cdleme19b  36030  cdleme21ct  36055  cdleme21d  36056  cdleme21e  36057  cdleme21k  36064  cdleme22g  36074  cdleme24  36078  cdleme27a  36093  cdleme27N  36095  cdleme28a  36096  cdleme40n  36194  cdlemg16zz  36386  cdlemg37  36415  cdlemk21-2N  36617  cdlemk20-2N  36618  cdlemk28-3  36634  cdlemk19xlem  36668
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 975
  Copyright terms: Public domain W3C validator