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

Theorem syl323anc 1258
 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
syl323anc.9
Assertion
Ref Expression
syl323anc

Proof of Theorem syl323anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . 2
3 sylXanc.3 . 2
4 sylXanc.4 . . 3
5 sylXanc.5 . . 3
64, 5jca 532 . 2
7 sylXanc.6 . 2
8 sylXanc.7 . 2
9 sylXanc.8 . 2
10 syl323anc.9 . 2
111, 2, 3, 6, 7, 8, 9, 10syl313anc 1252 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  /\w3a 973 This theorem is referenced by:  4atlem11  35333  dalem52  35448  dath2  35461  dalawlem1  35595  dalaw  35610  cdlemb2  35765  4atexlem7  35799  cdleme7ga  35973  cdleme18a  36016  cdleme18c  36018  cdleme21f  36058  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme27a  36093  cdlemg17dN  36389  cdlemg18a  36404  cdlemg31d  36426  cdlemg48  36463  cdlemj1  36547  dihord4  36985 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