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

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

Proof of Theorem syl233anc
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
31, 2jca 515 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl133anc.7 . 2 (𝜑𝜎)
9 syl233anc.8 . 2 (𝜑𝜌)
10 syl233anc.9 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ (𝜁𝜎𝜌)) → 𝜇)
113, 4, 5, 6, 7, 8, 9, 10syl133anc 1390 1 (𝜑𝜇)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 1086
This theorem is referenced by:  br8d  30347  2llnjN  36741  cdleme16b  37453  cdleme18d  37469  cdleme19d  37480  cdleme20bN  37484  cdleme20l1  37494  cdleme22cN  37516  cdleme22eALTN  37519  cdleme22f  37520  cdlemg33c0  37876  cdlemk5  38010  cdlemk5u  38035  cdlemky  38100  cdlemkyyN  38136
  Copyright terms: Public domain W3C validator