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 1128 . 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 395  w3a 1086
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 1088
This theorem is referenced by:  xpord3inddlem  8180  initoeu2lem2  18061  mdetunilem9  22627  mdetuni0  22628  xmetrtri  24366  bl2in  24411  blhalf  24416  blssps  24435  blss  24436  blcld  24519  methaus  24534  metdstri  24874  metdscnlem  24878  metnrmlem3  24884  xlebnum  24998  pmltpclem1  25484  colinearalglem2  28923  axlowdim  28977  ssbnd  37796  totbndbnd  37797  heiborlem6  37824  2atm  39530  lplncvrlvol2  39618  dalem19  39685  paddasslem9  39831  pclclN  39894  pclfinN  39903  pclfinclN  39953  pexmidlem8N  39980  trlval3  40190  cdleme22b  40344  cdlemefr29bpre0N  40409  cdlemefr29clN  40410  cdlemefr32fvaN  40412  cdlemefr32fva1  40413  cdlemg31b0N  40697  cdlemg31b0a  40698  cdlemh  40820  dihmeetlem16N  41325  dihmeetlem18N  41327  dihmeetlem19N  41328  dihmeetlem20N  41329  hoidmvlelem1  46615
  Copyright terms: Public domain W3C validator