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 513 . 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 397  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 206  df-an 398  df-3an 1090
This theorem is referenced by:  4atlem11  38122  dalem52  38237  dath2  38250  dalawlem1  38384  dalaw  38399  cdlemb2  38554  4atexlem7  38588  cdleme7ga  38761  cdleme18a  38804  cdleme18c  38806  cdleme21f  38845  cdleme26f2ALTN  38877  cdleme26f2  38878  cdleme27a  38880  cdlemg17dN  39176  cdlemg18a  39191  cdlemg31d  39213  cdlemg48  39250  cdlemj1  39334  dihord4  39771
  Copyright terms: Public domain W3C validator