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

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

Proof of Theorem syl323anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 554 . 2 (𝜑 → (𝜏𝜂))
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl133anc.7 . 2 (𝜑𝜎)
9 syl233anc.8 . 2 (𝜑𝜌)
10 syl323anc.9 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎𝜌)) → 𝜇)
111, 2, 3, 6, 7, 8, 9, 10syl313anc 1347 1 (𝜑𝜇)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  4atlem11  34372  dalem52  34487  dath2  34500  dalawlem1  34634  dalaw  34649  cdlemb2  34804  4atexlem7  34838  cdleme7ga  35012  cdleme18a  35055  cdleme18c  35057  cdleme21f  35097  cdleme26f2ALTN  35129  cdleme26f2  35130  cdleme27a  35132  cdlemg17dN  35428  cdlemg18a  35443  cdlemg31d  35465  cdlemg48  35502  cdlemj1  35586  dihord4  36024
  Copyright terms: Public domain W3C validator