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

Theorem syl331anc 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 (𝜑𝜁)
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 1125 . 2 (𝜑 → (𝜏𝜂𝜁))
8 syl133anc.7 . 2 (𝜑𝜎)
9 syl331anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ 𝜎) → 𝜌)
101, 2, 3, 7, 8, 9syl311anc 1381 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 1086
This theorem is referenced by:  syl332anc  1398  syl333anc  1399  qredeu  16659  brbtwn2  28839  3atlem4  39185  3atlem6  39187  llnexchb2  39568  osumcllem9N  39663  cdlemd4  39900  cdleme26fALTN  40061  cdleme26f  40062  cdleme36m  40160  cdlemg17b  40361  cdlemg17h  40367  cdlemk38  40614  cdlemk53b  40655  cdlemkyyN  40661  cdlemk43N  40662
  Copyright terms: Public domain W3C validator