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

Theorem syl231anc 1388
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 510 . 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 1381 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1085
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 395  df-3an 1087
This theorem is referenced by:  syl232anc  1395  isosctr  26562  axeuclid  28488  dalawlem3  39047  dalawlem6  39050  cdlemd7  39378  cdleme18c  39467  cdlemi  39994  cdlemk7  40022  cdlemk11  40023  cdlemk7u  40044  cdlemk11u  40045  cdlemk19xlem  40116  cdlemk55u1  40139  cdlemk56  40145
  Copyright terms: Public domain W3C validator