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

Theorem syl123anc 1388
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl123anc.7 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
Assertion
Ref Expression
syl123anc (𝜑𝜎)

Proof of Theorem syl123anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
42, 3jca 513 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl123anc.7 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
91, 4, 5, 6, 7, 8syl113anc 1383 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  dvfsumlem2  25544  noinfbnd2  27234  gg-dvfsumlem2  35183  atbtwnexOLDN  38318  atbtwnex  38319  osumcllem7N  38833  lhpmcvr5N  38898  cdleme22f2  39218  cdlemefs32sn1aw  39285  cdlemg7aN  39496  cdlemg7N  39497  cdlemg8c  39500  cdlemg8  39502  cdlemg11aq  39509  cdlemg12b  39515  cdlemg12e  39518  cdlemg12g  39520  cdlemg13a  39522  cdlemg15a  39526  cdlemg17e  39536  cdlemg18d  39552  cdlemg19a  39554  cdlemg20  39556  cdlemg22  39558  cdlemg28a  39564  cdlemg29  39576  cdlemg44a  39602  cdlemk34  39781  cdlemn11pre  40081  dihord10  40094  dihord2pre  40096  dihmeetlem17N  40194
  Copyright terms: Public domain W3C validator