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

Theorem syl123anc 1236
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
syl123anc.7
Assertion
Ref Expression
syl123anc

Proof of Theorem syl123anc
StepHypRef Expression
1 sylXanc.1 . 2
2 sylXanc.2 . . 3
3 sylXanc.3 . . 3
42, 3jca 532 . 2
5 sylXanc.4 . 2
6 sylXanc.5 . 2
7 sylXanc.6 . 2
8 syl123anc.7 . 2
91, 4, 5, 6, 7, 8syl113anc 1231 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 965
This theorem is referenced by:  dvfsumlem2  21899  atbtwnexOLDN  33942  atbtwnex  33943  osumcllem7N  34457  lhpmcvr5N  34522  cdleme22f2  34842  cdlemefs32sn1aw  34909  cdlemg7aN  35120  cdlemg7N  35121  cdlemg8c  35124  cdlemg8  35126  cdlemg11aq  35133  cdlemg12b  35139  cdlemg12e  35142  cdlemg12g  35144  cdlemg13a  35146  cdlemg15a  35150  cdlemg17e  35160  cdlemg18d  35176  cdlemg19a  35178  cdlemg20  35180  cdlemg22  35182  cdlemg28a  35188  cdlemg29  35200  cdlemg44a  35226  cdlemk34  35405  cdlemn11pre  35706  dihord10  35719  dihord2pre  35721  dihmeetlem17N  35819
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 967
  Copyright terms: Public domain W3C validator