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

Theorem syl33anc 1386
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 (𝜑𝜁)
syl33anc.7 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
Assertion
Ref Expression
syl33anc (𝜑𝜎)

Proof of Theorem syl33anc
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1129 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl33anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
94, 5, 6, 7, 8syl13anc 1373 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  xpord3inddlem  8087  initoeu2lem2  17902  mdetunilem9  21972  mdetuni0  21973  xmetrtri  23711  bl2in  23756  blhalf  23761  blssps  23780  blss  23781  blcld  23864  methaus  23879  metdstri  24217  metdscnlem  24221  metnrmlem3  24227  xlebnum  24331  pmltpclem1  24815  colinearalglem2  27859  axlowdim  27913  ssbnd  36250  totbndbnd  36251  heiborlem6  36278  2atm  37993  lplncvrlvol2  38081  dalem19  38148  paddasslem9  38294  pclclN  38357  pclfinN  38366  pclfinclN  38416  pexmidlem8N  38443  trlval3  38653  cdleme22b  38807  cdlemefr29bpre0N  38872  cdlemefr29clN  38873  cdlemefr32fvaN  38875  cdlemefr32fva1  38876  cdlemg31b0N  39160  cdlemg31b0a  39161  cdlemh  39283  dihmeetlem16N  39788  dihmeetlem18N  39790  dihmeetlem19N  39791  dihmeetlem20N  39792  hoidmvlelem1  44843
  Copyright terms: Public domain W3C validator