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

Theorem syl123anc 1389
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 515 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl123anc.7 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
91, 4, 5, 6, 7, 8syl113anc 1384 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089
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 210  df-an 400  df-3an 1091
This theorem is referenced by:  dvfsumlem2  24924  noinfbnd2  33671  atbtwnexOLDN  37198  atbtwnex  37199  osumcllem7N  37713  lhpmcvr5N  37778  cdleme22f2  38098  cdlemefs32sn1aw  38165  cdlemg7aN  38376  cdlemg7N  38377  cdlemg8c  38380  cdlemg8  38382  cdlemg11aq  38389  cdlemg12b  38395  cdlemg12e  38398  cdlemg12g  38400  cdlemg13a  38402  cdlemg15a  38406  cdlemg17e  38416  cdlemg18d  38432  cdlemg19a  38434  cdlemg20  38436  cdlemg22  38438  cdlemg28a  38444  cdlemg29  38456  cdlemg44a  38482  cdlemk34  38661  cdlemn11pre  38961  dihord10  38974  dihord2pre  38976  dihmeetlem17N  39074
  Copyright terms: Public domain W3C validator