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

Theorem syl33anc 1382
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 1125 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl33anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
94, 5, 6, 7, 8syl13anc 1369 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 396  df-3an 1086
This theorem is referenced by:  xpord3inddlem  8134  initoeu2lem2  17967  mdetunilem9  22444  mdetuni0  22445  xmetrtri  24183  bl2in  24228  blhalf  24233  blssps  24252  blss  24253  blcld  24336  methaus  24351  metdstri  24689  metdscnlem  24693  metnrmlem3  24699  xlebnum  24813  pmltpclem1  25299  colinearalglem2  28634  axlowdim  28688  ssbnd  37146  totbndbnd  37147  heiborlem6  37174  2atm  38888  lplncvrlvol2  38976  dalem19  39043  paddasslem9  39189  pclclN  39252  pclfinN  39261  pclfinclN  39311  pexmidlem8N  39338  trlval3  39548  cdleme22b  39702  cdlemefr29bpre0N  39767  cdlemefr29clN  39768  cdlemefr32fvaN  39770  cdlemefr32fva1  39771  cdlemg31b0N  40055  cdlemg31b0a  40056  cdlemh  40178  dihmeetlem16N  40683  dihmeetlem18N  40685  dihmeetlem19N  40686  dihmeetlem20N  40687  hoidmvlelem1  45796
  Copyright terms: Public domain W3C validator