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

Theorem syl231anc 1392
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 1385 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  syl232anc  1399  isosctr  26864  axeuclid  28978  dalawlem3  39875  dalawlem6  39878  cdlemd7  40206  cdleme18c  40295  cdlemi  40822  cdlemk7  40850  cdlemk11  40851  cdlemk7u  40872  cdlemk11u  40873  cdlemk19xlem  40944  cdlemk55u1  40967  cdlemk56  40973
  Copyright terms: Public domain W3C validator