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

Theorem syl323anc 1507
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 (𝜑𝜁)
syl133anc.7 (𝜑𝜎)
syl233anc.8 (𝜑𝜌)
syl323anc.9 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎𝜌)) → 𝜇)
Assertion
Ref Expression
syl323anc (𝜑𝜇)

Proof of Theorem syl323anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 555 . 2 (𝜑 → (𝜏𝜂))
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl133anc.7 . 2 (𝜑𝜎)
9 syl233anc.8 . 2 (𝜑𝜌)
10 syl323anc.9 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎𝜌)) → 𝜇)
111, 2, 3, 6, 7, 8, 9, 10syl313anc 1501 1 (𝜑𝜇)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  4atlem11  35396  dalem52  35511  dath2  35524  dalawlem1  35658  dalaw  35673  cdlemb2  35828  4atexlem7  35862  cdleme7ga  36036  cdleme18a  36079  cdleme18c  36081  cdleme21f  36120  cdleme26f2ALTN  36152  cdleme26f2  36153  cdleme27a  36155  cdlemg17dN  36451  cdlemg18a  36466  cdlemg31d  36488  cdlemg48  36525  cdlemj1  36609  dihord4  37047
  Copyright terms: Public domain W3C validator