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 510 . 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 394  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 206  df-an 395  df-3an 1086
This theorem is referenced by:  br8d  32421  2llnjN  39072  cdleme16b  39784  cdleme18d  39800  cdleme19d  39811  cdleme20bN  39815  cdleme20l1  39825  cdleme22cN  39847  cdleme22eALTN  39850  cdleme22f  39851  cdlemg33c0  40207  cdlemk5  40341  cdlemk5u  40366  cdlemky  40431  cdlemkyyN  40467
  Copyright terms: Public domain W3C validator