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

Theorem syl331anc 1393
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 (𝜑𝜁)
syl133anc.7 (𝜑𝜎)
syl331anc.8 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ 𝜎) → 𝜌)
Assertion
Ref Expression
syl331anc (𝜑𝜌)

Proof of Theorem syl331anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
74, 5, 63jca 1126 . 2 (𝜑 → (𝜏𝜂𝜁))
8 syl133anc.7 . 2 (𝜑𝜎)
9 syl331anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ 𝜎) → 𝜌)
101, 2, 3, 7, 8, 9syl311anc 1382 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  syl332anc  1399  syl333anc  1400  qredeu  16599  brbtwn2  28430  3atlem4  38660  3atlem6  38662  llnexchb2  39043  osumcllem9N  39138  cdlemd4  39375  cdleme26fALTN  39536  cdleme26f  39537  cdleme36m  39635  cdlemg17b  39836  cdlemg17h  39842  cdlemk38  40089  cdlemk53b  40130  cdlemkyyN  40136  cdlemk43N  40137
  Copyright terms: Public domain W3C validator