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

Theorem syl33anc 1510
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 1164 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl33anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
94, 5, 6, 7, 8syl13anc 1497 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1113
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 199  df-an 387  df-3an 1115
This theorem is referenced by:  initoeu2lem2  17017  mdetunilem9  20794  mdetuni0  20795  xmetrtri  22530  bl2in  22575  blhalf  22580  blssps  22599  blss  22600  blcld  22680  methaus  22695  metdstri  23024  metdscnlem  23028  metnrmlem3  23034  xlebnum  23134  pmltpclem1  23614  colinearalglem2  26206  axlowdim  26260  ssbnd  34129  totbndbnd  34130  heiborlem6  34157  2atm  35602  lplncvrlvol2  35690  dalem19  35757  paddasslem9  35903  pclclN  35966  pclfinN  35975  pclfinclN  36025  pexmidlem8N  36052  trlval3  36262  cdleme22b  36416  cdlemefr29bpre0N  36481  cdlemefr29clN  36482  cdlemefr32fvaN  36484  cdlemefr32fva1  36485  cdlemg31b0N  36769  cdlemg31b0a  36770  cdlemh  36892  dihmeetlem16N  37397  dihmeetlem18N  37399  dihmeetlem19N  37400  dihmeetlem20N  37401  hoidmvlelem1  41603
  Copyright terms: Public domain W3C validator