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

Theorem syl322anc 1390
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 512 . 2 (𝜑 → (𝜁𝜎))
9 syl322anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ (𝜁𝜎)) → 𝜌)
101, 2, 3, 4, 5, 8, 9syl321anc 1384 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  ax5seglem6  26647  ax5seg  26651  elpaddatriN  36819  paddasslem8  36843  paddasslem12  36847  paddasslem13  36848  pmodlem1  36862  osumcllem5N  36976  pexmidlem2N  36987  cdleme3h  37251  cdleme7ga  37264  cdleme20l  37338  cdleme21ct  37345  cdleme21d  37346  cdleme21e  37347  cdleme26e  37375  cdleme26eALTN  37377  cdleme26fALTN  37378  cdleme26f  37379  cdleme26f2ALTN  37380  cdleme26f2  37381  cdleme39n  37482  cdlemh2  37832  cdlemh  37833  cdlemk12  37866  cdlemk12u  37888  cdlemkfid1N  37937  congsub  39445  mzpcong  39447  jm2.18  39463  jm2.15nn0  39478  jm2.27c  39482
  Copyright terms: Public domain W3C validator