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

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

Proof of Theorem syl323anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 515 . 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 1395 1 (𝜑𝜇)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1088
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 1090
This theorem is referenced by:  4atlem11  37235  dalem52  37350  dath2  37363  dalawlem1  37497  dalaw  37512  cdlemb2  37667  4atexlem7  37701  cdleme7ga  37874  cdleme18a  37917  cdleme18c  37919  cdleme21f  37958  cdleme26f2ALTN  37990  cdleme26f2  37991  cdleme27a  37993  cdlemg17dN  38289  cdlemg18a  38304  cdlemg31d  38326  cdlemg48  38363  cdlemj1  38447  dihord4  38884
  Copyright terms: Public domain W3C validator