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

Theorem syl233anc 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 (𝜑𝜌)
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 1395 1 (𝜑𝜇)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089
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 1091
This theorem is referenced by:  br8d  30693  2llnjN  37344  cdleme16b  38056  cdleme18d  38072  cdleme19d  38083  cdleme20bN  38087  cdleme20l1  38097  cdleme22cN  38119  cdleme22eALTN  38122  cdleme22f  38123  cdlemg33c0  38479  cdlemk5  38613  cdlemk5u  38638  cdlemky  38703  cdlemkyyN  38739
  Copyright terms: Public domain W3C validator