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

Theorem syl331anc 1391
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 1124 . 2 (𝜑 → (𝜏𝜂𝜁))
8 syl133anc.7 . 2 (𝜑𝜎)
9 syl331anc.8 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁) ∧ 𝜎) → 𝜌)
101, 2, 3, 7, 8, 9syl311anc 1380 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  syl332anc  1397  syl333anc  1398  qredeu  16001  brbtwn2  26690  3atlem4  36621  3atlem6  36623  llnexchb2  37004  osumcllem9N  37099  cdlemd4  37336  cdleme26fALTN  37497  cdleme26f  37498  cdleme36m  37596  cdlemg17b  37797  cdlemg17h  37803  cdlemk38  38050  cdlemk53b  38091  cdlemkyyN  38097  cdlemk43N  38098
  Copyright terms: Public domain W3C validator