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

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

Proof of Theorem syl311anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
3 sylXanc.3 . . 3
41, 2, 33jca 1176 . 2
5 sylXanc.4 . 2
6 sylXanc.5 . 2
7 syl311anc.6 . 2
84, 5, 6, 7syl3anc 1228 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  syl312anc  1249  syl321anc  1250  syl313anc  1252  syl331anc  1253  pythagtrip  14358  nmolb2d  21225  nmoleub  21238  clwwisshclwwlem  24806  cvlcvr1  35064  4atlem12b  35335  dalawlem10  35604  dalawlem13  35607  dalawlem15  35609  osumcllem11N  35690  lhp2atne  35758  lhp2at0ne  35760  cdlemd  35932  ltrneq3  35933  cdleme7d  35971  cdlemeg49le  36237  cdleme  36286  cdlemg1a  36296  ltrniotavalbN  36310  cdlemg44  36459  cdlemk19  36595  cdlemk27-3  36633  cdlemk33N  36635  cdlemk34  36636  cdlemk49  36677  cdlemk53a  36681  cdlemk19u  36696  cdlemk56w  36699  dia2dimlem4  36794  dih1dimatlem0  37055
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