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

Theorem syl321anc 1392
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 512 . 2 (𝜑 → (𝜏𝜂))
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl321anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ 𝜁) → 𝜎)
91, 2, 3, 6, 7, 8syl311anc 1384 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  syl322anc  1398  cxple2ad  26240  chordthmlem3  26346  nosupbnd1lem3  27220  nosupbnd1lem4  27221  noinfbnd1lem3  27235  noinfbnd1lem4  27236  4noncolr2  38411  4noncolr1  38412  3atlem5  38444  2lplnj  38577  llnmod2i2  38820  dalawlem11  38838  dalawlem12  38839  cdleme43dN  39449  cdleme4gfv  39464  cdlemeg46nlpq  39474  cdlemg17bq  39630  cdlemg31b0N  39651  cdlemg31b0a  39652  cdlemg31c  39656  cdlemg39  39673  cdlemk47  39906  lincext3  47215
  Copyright terms: Public domain W3C validator