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

Theorem syl123anc 1499
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 503 . 2 (𝜑 → (𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl123anc.7 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
91, 4, 5, 6, 7, 8syl113anc 1494 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  dvfsumlem2  24010  atbtwnexOLDN  35229  atbtwnex  35230  osumcllem7N  35744  lhpmcvr5N  35809  cdleme22f2  36129  cdlemefs32sn1aw  36196  cdlemg7aN  36407  cdlemg7N  36408  cdlemg8c  36411  cdlemg8  36413  cdlemg11aq  36420  cdlemg12b  36426  cdlemg12e  36429  cdlemg12g  36431  cdlemg13a  36433  cdlemg15a  36437  cdlemg17e  36447  cdlemg18d  36463  cdlemg19a  36465  cdlemg20  36467  cdlemg22  36469  cdlemg28a  36475  cdlemg29  36487  cdlemg44a  36513  cdlemk34  36692  cdlemn11pre  36992  dihord10  37005  dihord2pre  37007  dihmeetlem17N  37105
  Copyright terms: Public domain W3C validator