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

Theorem syl231anc 1383
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 (𝜑𝜁)
syl231anc.7 (((𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ 𝜁) → 𝜎)
Assertion
Ref Expression
syl231anc (𝜑𝜎)

Proof of Theorem syl231anc
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
31, 2jca 512 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl231anc.7 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ 𝜁) → 𝜎)
93, 4, 5, 6, 7, 8syl131anc 1376 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080
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 1082
This theorem is referenced by:  syl232anc  1390  isosctr  25080  axeuclid  26432  dalawlem3  36540  dalawlem6  36543  cdlemd7  36871  cdleme18c  36960  cdlemi  37487  cdlemk7  37515  cdlemk11  37516  cdlemk7u  37537  cdlemk11u  37538  cdlemk19xlem  37609  cdlemk55u1  37632  cdlemk56  37638
  Copyright terms: Public domain W3C validator