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

Theorem syl322anc 1345
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 552 . 2 (𝜑 → (𝜁𝜎))
9 syl322anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 5, 8, 9syl321anc 1339 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  ax5seglem6  25532  ax5seg  25536  elpaddatriN  33910  paddasslem8  33934  paddasslem12  33938  paddasslem13  33939  pmodlem1  33953  osumcllem5N  34067  pexmidlem2N  34078  cdleme3h  34343  cdleme7ga  34356  cdleme20l  34431  cdleme21ct  34438  cdleme21d  34439  cdleme21e  34440  cdleme26e  34468  cdleme26eALTN  34470  cdleme26fALTN  34471  cdleme26f  34472  cdleme26f2ALTN  34473  cdleme26f2  34474  cdleme39n  34575  cdlemh2  34925  cdlemh  34926  cdlemk12  34959  cdlemk12u  34981  cdlemkfid1N  35030  congsub  36358  mzpcong  36360  jm2.18  36376  jm2.15nn0  36391  jm2.27c  36395
  Copyright terms: Public domain W3C validator