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

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

Proof of Theorem syl332anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . 2 (𝜑𝜂)
6 syl33anc.6 . 2 (𝜑𝜁)
7 syl133anc.7 . . 3 (𝜑𝜎)
8 syl233anc.8 . . 3 (𝜑𝜌)
97, 8jca 511 . 2 (𝜑 → (𝜎𝜌))
10 syl332anc.9 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ (𝜎𝜌)) → 𝜇)
111, 2, 3, 4, 5, 6, 9, 10syl331anc 1396 1 (𝜑𝜇)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  mdetunilem5  22623  mdetuni0  22628  lnjatN  39783  lncmp  39786  cdlema1N  39794  4atexlemex6  40077  cdlemd4  40204  cdleme18c  40296  cdleme18d  40298  cdleme19b  40307  cdleme21ct  40332  cdleme21d  40333  cdleme21e  40334  cdleme21k  40341  cdleme22g  40351  cdleme24  40355  cdleme27a  40370  cdleme27N  40372  cdleme28a  40373  cdleme40n  40471  cdlemg16zz  40663  cdlemg37  40692  cdlemk21-2N  40894  cdlemk20-2N  40895  cdlemk28-3  40911  cdlemk19xlem  40945
  Copyright terms: Public domain W3C validator