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

Theorem syl123anc 1379
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 512 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl123anc.7 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
91, 4, 5, 6, 7, 8syl113anc 1374 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  dvfsumlem2  24551  atbtwnexOLDN  36463  atbtwnex  36464  osumcllem7N  36978  lhpmcvr5N  37043  cdleme22f2  37363  cdlemefs32sn1aw  37430  cdlemg7aN  37641  cdlemg7N  37642  cdlemg8c  37645  cdlemg8  37647  cdlemg11aq  37654  cdlemg12b  37660  cdlemg12e  37663  cdlemg12g  37665  cdlemg13a  37667  cdlemg15a  37671  cdlemg17e  37681  cdlemg18d  37697  cdlemg19a  37699  cdlemg20  37701  cdlemg22  37703  cdlemg28a  37709  cdlemg29  37721  cdlemg44a  37747  cdlemk34  37926  cdlemn11pre  38226  dihord10  38239  dihord2pre  38241  dihmeetlem17N  38339
  Copyright terms: Public domain W3C validator