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

Theorem syl321anc 1389
 Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl321anc.7 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ 𝜁) → 𝜎)
Assertion
Ref Expression
syl321anc (𝜑𝜎)

Proof of Theorem syl321anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 515 . 2 (𝜑 → (𝜏𝜂))
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl321anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ 𝜁) → 𝜎)
91, 2, 3, 6, 7, 8syl311anc 1381 1 (𝜑𝜎)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  syl322anc  1395  cxple2ad  25326  chordthmlem3  25430  nosupbnd1lem3  33338  nosupbnd1lem4  33339  4noncolr2  36769  4noncolr1  36770  3atlem5  36802  2lplnj  36935  llnmod2i2  37178  dalawlem11  37196  dalawlem12  37197  cdleme43dN  37807  cdleme4gfv  37822  cdlemeg46nlpq  37832  cdlemg17bq  37988  cdlemg31b0N  38009  cdlemg31b0a  38010  cdlemg31c  38014  cdlemg39  38031  cdlemk47  38264  lincext3  44906
 Copyright terms: Public domain W3C validator