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

Theorem syl233anc 1347
 Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl133anc.7 (𝜑𝜎)
syl233anc.8 (𝜑𝜌)
syl233anc.9 (((𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ (𝜁𝜎𝜌)) → 𝜇)
Assertion
Ref Expression
syl233anc (𝜑𝜇)

Proof of Theorem syl233anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
31, 2jca 553 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.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 1341 1 (𝜑𝜇)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  br8d  28802  2llnjN  33871  cdleme16b  34584  cdleme18d  34600  cdleme19d  34612  cdleme20bN  34616  cdleme20l1  34626  cdleme22cN  34648  cdleme22eALTN  34651  cdleme22f  34652  cdlemg33c0  35008  cdlemk5  35142  cdlemk5u  35167  cdlemky  35232  cdlemkyyN  35268
 Copyright terms: Public domain W3C validator