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

Theorem syl123anc 1245
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 1240 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  dvfsumlem2  22428  atbtwnexOLDN  35171  atbtwnex  35172  osumcllem7N  35686  lhpmcvr5N  35751  cdleme22f2  36073  cdlemefs32sn1aw  36140  cdlemg7aN  36351  cdlemg7N  36352  cdlemg8c  36355  cdlemg8  36357  cdlemg11aq  36364  cdlemg12b  36370  cdlemg12e  36373  cdlemg12g  36375  cdlemg13a  36377  cdlemg15a  36381  cdlemg17e  36391  cdlemg18d  36407  cdlemg19a  36409  cdlemg20  36411  cdlemg22  36413  cdlemg28a  36419  cdlemg29  36431  cdlemg44a  36457  cdlemk34  36636  cdlemn11pre  36937  dihord10  36950  dihord2pre  36952  dihmeetlem17N  37050
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