Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl322anc Structured version   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  25873  ax5seg  25877  congsub  27035  mzpcong  27037  jm2.18  27059  jm2.15nn0  27074  jm2.27c  27078  elpaddatriN  30600  paddasslem8  30624  paddasslem12  30628  paddasslem13  30629  pmodlem1  30643  osumcllem5N  30757  pexmidlem2N  30768  cdleme3h  31032  cdleme7ga  31045  cdleme20l  31119  cdleme21ct  31126  cdleme21d  31127  cdleme21e  31128  cdleme26e  31156  cdleme26eALTN  31158  cdleme26fALTN  31159  cdleme26f  31160  cdleme26f2ALTN  31161  cdleme26f2  31162  cdleme39n  31263  cdlemh2  31613  cdlemh  31614  cdlemk12  31647  cdlemk12u  31669  cdlemkfid1N  31718 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