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

Theorem syl322anc 1505
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 (𝜑𝜎)
syl322anc.8 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎)) → 𝜌)
Assertion
Ref Expression
syl322anc (𝜑𝜌)

Proof of Theorem syl322anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . 2 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
7 syl133anc.7 . . 3 (𝜑𝜎)
86, 7jca 555 . 2 (𝜑 → (𝜁𝜎))
9 syl322anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 5, 8, 9syl321anc 1499 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  ax5seglem6  26013  ax5seg  26017  elpaddatriN  35592  paddasslem8  35616  paddasslem12  35620  paddasslem13  35621  pmodlem1  35635  osumcllem5N  35749  pexmidlem2N  35760  cdleme3h  36025  cdleme7ga  36038  cdleme20l  36112  cdleme21ct  36119  cdleme21d  36120  cdleme21e  36121  cdleme26e  36149  cdleme26eALTN  36151  cdleme26fALTN  36152  cdleme26f  36153  cdleme26f2ALTN  36154  cdleme26f2  36155  cdleme39n  36256  cdlemh2  36606  cdlemh  36607  cdlemk12  36640  cdlemk12u  36662  cdlemkfid1N  36711  congsub  38039  mzpcong  38041  jm2.18  38057  jm2.15nn0  38072  jm2.27c  38076
  Copyright terms: Public domain W3C validator