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

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

Proof of Theorem syl321anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . 2 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
64, 5jca 495 . 2 (𝜑 → (𝜏𝜂))
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl321anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂) ∧ 𝜁) → 𝜎)
91, 2, 3, 6, 7, 8syl311anc 1489 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1070
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 383  df-3an 1072
This theorem is referenced by:  syl322anc  1503  cxple2ad  24691  chordthmlem3  24781  nosupbnd1lem3  32187  nosupbnd1lem4  32188  4noncolr2  35255  4noncolr1  35256  3atlem5  35288  2lplnj  35421  llnmod2i2  35664  dalawlem11  35682  dalawlem12  35683  cdleme43dN  36294  cdleme4gfv  36309  cdlemeg46nlpq  36319  cdlemg17bq  36475  cdlemg31b0N  36496  cdlemg31b0a  36497  cdlemg31c  36501  cdlemg39  36518  cdlemk47  36751  lincext3  42763
  Copyright terms: Public domain W3C validator