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

Theorem syl322anc 1394
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 553 . 2 (𝜑 → (𝜁𝜎))
9 syl322anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 5, 8, 9syl321anc 1388 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  ax5seglem6  25859  ax5seg  25863  elpaddatriN  35407  paddasslem8  35431  paddasslem12  35435  paddasslem13  35436  pmodlem1  35450  osumcllem5N  35564  pexmidlem2N  35575  cdleme3h  35840  cdleme7ga  35853  cdleme20l  35927  cdleme21ct  35934  cdleme21d  35935  cdleme21e  35936  cdleme26e  35964  cdleme26eALTN  35966  cdleme26fALTN  35967  cdleme26f  35968  cdleme26f2ALTN  35969  cdleme26f2  35970  cdleme39n  36071  cdlemh2  36421  cdlemh  36422  cdlemk12  36455  cdlemk12u  36477  cdlemkfid1N  36526  congsub  37854  mzpcong  37856  jm2.18  37872  jm2.15nn0  37887  jm2.27c  37891
  Copyright terms: Public domain W3C validator