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

Theorem syl322anc 1212
 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
syl322anc.8
Assertion
Ref Expression
syl322anc

Proof of Theorem syl322anc
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 . . 3
7 sylXanc.7 . . 3
86, 7jca 519 . 2
9 syl322anc.8 . 2
101, 2, 3, 4, 5, 8, 9syl321anc 1206 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   w3a 936 This theorem is referenced by:  ax5seglem6  25746  ax5seg  25750  congsub  26887  mzpcong  26889  jm2.18  26911  jm2.15nn0  26926  jm2.27c  26930  elpaddatriN  30225  paddasslem8  30249  paddasslem12  30253  paddasslem13  30254  pmodlem1  30268  osumcllem5N  30382  pexmidlem2N  30393  cdleme3h  30657  cdleme7ga  30670  cdleme20l  30744  cdleme21ct  30751  cdleme21d  30752  cdleme21e  30753  cdleme26e  30781  cdleme26eALTN  30783  cdleme26fALTN  30784  cdleme26f  30785  cdleme26f2ALTN  30786  cdleme26f2  30787  cdleme39n  30888  cdlemh2  31238  cdlemh  31239  cdlemk12  31272  cdlemk12u  31294  cdlemkfid1N  31343 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