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

Theorem syl231anc 1389
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 511 . 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 1382 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 396  df-3an 1088
This theorem is referenced by:  syl232anc  1396  isosctr  26667  axeuclid  28654  dalawlem3  39208  dalawlem6  39211  cdlemd7  39539  cdleme18c  39628  cdlemi  40155  cdlemk7  40183  cdlemk11  40184  cdlemk7u  40205  cdlemk11u  40206  cdlemk19xlem  40277  cdlemk55u1  40300  cdlemk56  40306
  Copyright terms: Public domain W3C validator