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

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

Proof of Theorem syl231anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
31, 2jca 501 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl231anc.7 . 2 (((𝜓𝜒) ∧ (𝜃𝜏𝜂) ∧ 𝜁) → 𝜎)
93, 4, 5, 6, 7, 8syl131anc 1489 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 1073
This theorem is referenced by:  syl232anc  1503  isosctr  24772  axeuclid  26064  dalawlem3  35681  dalawlem6  35684  cdlemd7  36013  cdleme18c  36102  cdlemi  36629  cdlemk7  36657  cdlemk11  36658  cdlemk7u  36679  cdlemk11u  36680  cdlemk19xlem  36751  cdlemk55u1  36774  cdlemk56  36780
  Copyright terms: Public domain W3C validator