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

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

Proof of Theorem syl123anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
42, 3jca 553 . 2 (𝜑 → (𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl123anc.7 . 2 ((𝜓 ∧ (𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
91, 4, 5, 6, 7, 8syl113anc 1330 1 (𝜑𝜎)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  dvfsumlem2  23594  atbtwnexOLDN  33751  atbtwnex  33752  osumcllem7N  34266  lhpmcvr5N  34331  cdleme22f2  34653  cdlemefs32sn1aw  34720  cdlemg7aN  34931  cdlemg7N  34932  cdlemg8c  34935  cdlemg8  34937  cdlemg11aq  34944  cdlemg12b  34950  cdlemg12e  34953  cdlemg12g  34955  cdlemg13a  34957  cdlemg15a  34961  cdlemg17e  34971  cdlemg18d  34987  cdlemg19a  34989  cdlemg20  34991  cdlemg22  34993  cdlemg28a  34999  cdlemg29  35011  cdlemg44a  35037  cdlemk34  35216  cdlemn11pre  35517  dihord10  35530  dihord2pre  35532  dihmeetlem17N  35630
 Copyright terms: Public domain W3C validator