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

Theorem syl322anc 1256
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 532 . 2
9 syl322anc.8 . 2
101, 2, 3, 4, 5, 8, 9syl321anc 1250 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  ax5seglem6  24237  ax5seg  24241  congsub  30908  mzpcong  30910  jm2.18  30930  jm2.15nn0  30945  jm2.27c  30949  elpaddatriN  35527  paddasslem8  35551  paddasslem12  35555  paddasslem13  35556  pmodlem1  35570  osumcllem5N  35684  pexmidlem2N  35695  cdleme3h  35960  cdleme7ga  35973  cdleme20l  36048  cdleme21ct  36055  cdleme21d  36056  cdleme21e  36057  cdleme26e  36085  cdleme26eALTN  36087  cdleme26fALTN  36088  cdleme26f  36089  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme39n  36192  cdlemh2  36542  cdlemh  36543  cdlemk12  36576  cdlemk12u  36598  cdlemkfid1N  36647
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