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

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

Proof of Theorem syl322anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . 2 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
7 syl133anc.7 . . 3 (𝜑𝜎)
86, 7jca 508 . 2 (𝜑 → (𝜁𝜎))
9 syl322anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 5, 8, 9syl321anc 1512 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  ax5seglem6  26175  ax5seg  26179  elpaddatriN  35828  paddasslem8  35852  paddasslem12  35856  paddasslem13  35857  pmodlem1  35871  osumcllem5N  35985  pexmidlem2N  35996  cdleme3h  36260  cdleme7ga  36273  cdleme20l  36347  cdleme21ct  36354  cdleme21d  36355  cdleme21e  36356  cdleme26e  36384  cdleme26eALTN  36386  cdleme26fALTN  36387  cdleme26f  36388  cdleme26f2ALTN  36389  cdleme26f2  36390  cdleme39n  36491  cdlemh2  36841  cdlemh  36842  cdlemk12  36875  cdlemk12u  36897  cdlemkfid1N  36946  congsub  38326  mzpcong  38328  jm2.18  38344  jm2.15nn0  38359  jm2.27c  38363
  Copyright terms: Public domain W3C validator