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

Theorem syl33anc 1338
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl33anc.6 (𝜑𝜁)
syl33anc.7 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
Assertion
Ref Expression
syl33anc (𝜑𝜎)

Proof of Theorem syl33anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1240 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl33anc.6 . 2 (𝜑𝜁)
8 syl33anc.7 . 2 (((𝜓𝜒𝜃) ∧ (𝜏𝜂𝜁)) → 𝜎)
94, 5, 6, 7, 8syl13anc 1325 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  initoeu2lem2  16586  mdetunilem9  20345  mdetuni0  20346  xmetrtri  22070  bl2in  22115  blhalf  22120  blssps  22139  blss  22140  blcld  22220  methaus  22235  metdstri  22562  metdscnlem  22566  metnrmlem3  22572  xlebnum  22672  pmltpclem1  23124  colinearalglem2  25687  axlowdim  25741  ssbnd  33219  totbndbnd  33220  heiborlem6  33247  2atm  34293  lplncvrlvol2  34381  dalem19  34448  paddasslem9  34594  pclclN  34657  pclfinN  34666  pclfinclN  34716  pexmidlem8N  34743  trlval3  34954  cdleme22b  35109  cdlemefr29bpre0N  35174  cdlemefr29clN  35175  cdlemefr32fvaN  35177  cdlemefr32fva1  35178  cdlemg31b0N  35462  cdlemg31b0a  35463  cdlemh  35585  dihmeetlem16N  36091  dihmeetlem18N  36093  dihmeetlem19N  36094  dihmeetlem20N  36095  hoidmvlelem1  40116
  Copyright terms: Public domain W3C validator